diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+BSD 3-Clause License
+
+Copyright (c) 2021, Mikael Tönnberg
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+   contributors may be used to endorse or promote products derived from
+   this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,49 @@
+# Servant ❤️ GDP
+
+## In a nutshell
+To get more productive, produce high-quality web APIs and reduce the number of needed tests we can combine [Servant](https://haskell-servant.github.io/) (A web api framework) and [GDP](https://kataskeue.com/gdp.pdf) (Ghosts of Departed Proofs). This allows for quite expressive API declarations which leads to more [knowledge captured](https://carboncloud.com/2020/12/07/tech-knowledge-as-code/).
+[See a full example](https://github.com/mtonnberg/gdp-demo).
+
+```haskell
+-- http://localhost/div/10/5 would return 2
+type DivWebApi numerator denominator =
+  "div"
+    :> CaptureNamed (Int ~~ numerator 
+                    ::: IsPositive numerator)
+    :> CaptureNamed (Int ~~ denominator
+                    ::: IsPositive denominator)
+    :> Get
+         '[JSON]
+         ( Int ? IsEqualOrLessThan numerator
+         )
+```
+or
+```haskell
+-- http://localhost/habitats/savanna/animals/3
+-- could return ["lion", "elephant"]
+type GetAnimalsForHabitat user habitat pagesize =
+  AuthProtect "normalUser"
+    :> "habitats"
+    :> CaptureNamed (String ~~ habitat ::: IsNonEmpty habitat && IsTrimmed habitat)
+    :> "animals"
+    :> CaptureNamed (Int ~~ pagesize ::: IsPositive pagesize)
+    :> Get
+         '[JSON]
+         ( ( [String ? IsAValidatedAnimal habitat] ? HasAMaximumLengthOf pagesize
+           )
+             ::: user `HasAccessToHabitat` habitat
+         )
+```
+
+See <https://github.com/mtonnberg/gdp-demo> for a full, working example.
+
+## How does it work
+API-input is captured as named variables, making the named contexts span the entire request.
+This in turn, makes it possible to express a lot of domain knowledge/requirements  in the Servant API type.
+
+## Why does this exist?
+To both make the API-capabilities clearer and to make it easier to implement.
+
+It is often quite easy to identify domain rules, invariants and preconditions for the API but hard to capture that knowledge in the types. Instead a lot of domain rules and requirements are hidden in the implementation logic.
+
+Moving information to the types are in line with Knowledge-as-Code, read more about the benefits here: [Knowledge-as-Code](https://carboncloud.com/2020/12/07/tech-knowledge-as-code/)
diff --git a/servant-gdp.cabal b/servant-gdp.cabal
new file mode 100644
--- /dev/null
+++ b/servant-gdp.cabal
@@ -0,0 +1,40 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.34.4.
+--
+-- see: https://github.com/sol/hpack
+
+name:           servant-gdp
+version:        0.0.1.2
+synopsis:       Use Servant and GDP together to create expressive web API types
+description:    Servant (A web api framework) and GDP (Ghosts of Departed Proofs) is here combined to allow for quite expressive API declarations. This is achieved by parsing captured API-input as named variables, making the named contexts span the entire request. This in turn, makes it possible to express a lot of domain knowledge or requirements in the Servant API type. For an example of how this can look like check out <https://github.com/mtonnberg/gdp-demo>
+category:       Lib
+homepage:       https://github.com/mtonnberg/servant-gdp#readme
+author:         Mikael Tönnberg
+maintainer:     mikael@carboncloud.com
+copyright:      2021 Mikael Tönnberg
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+
+source-repository head
+  type: git
+  location: https://github.com/mtonnberg/servant-gdp
+
+library
+  exposed-modules:
+      Servant.GDP
+  other-modules:
+      Servant.GDP.ApiNamedInput
+      Servant.GDP.ProveInIsolation
+  hs-source-dirs:
+      src
+  build-depends:
+      aeson ==1.5.*
+    , base >=4.7 && <5
+    , gdp <0.1
+    , servant-server ==0.18.*
+    , text ==1.2.*
+  default-language: Haskell2010
diff --git a/src/Servant/GDP.hs b/src/Servant/GDP.hs
new file mode 100644
--- /dev/null
+++ b/src/Servant/GDP.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module Servant.GDP
+  ( module Servant.GDP.ApiNamedInput,
+    module Servant.GDP.ProveInIsolation,
+  )
+where
+
+import Servant.GDP.ApiNamedInput
+import Servant.GDP.ProveInIsolation
+
+import Data.Aeson (ToJSON, toJSON)
+import GDP (exorcise, rename, the, type (:::), type (?), type (~~))
+
+instance (ToJSON a) => ToJSON (a ~~ p) where
+  toJSON = toJSON . the
+
+instance (ToJSON a) => ToJSON (a ::: p) where
+  toJSON = toJSON . exorcise
+
+instance (ToJSON a) => ToJSON (a ? p) where
+  toJSON x =
+    rename x toJSON
diff --git a/src/Servant/GDP/ApiNamedInput.hs b/src/Servant/GDP/ApiNamedInput.hs
new file mode 100644
--- /dev/null
+++ b/src/Servant/GDP/ApiNamedInput.hs
@@ -0,0 +1,202 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module Servant.GDP.ApiNamedInput
+  ( ApiName0,
+    ApiName1,
+    ApiName2,
+    ApiName3,
+    ApiName4,
+    ApiName6,
+    ApiName7,
+    ApiName8,
+    ApiName9,
+    ApiName10,
+    ApiName11,
+    ApiName12,
+    ApiName13,
+    ApiName14,
+    ApiName15,
+    ApiName16,
+    ApiName17,
+    ApiName18,
+    ApiName19,
+    ApiName20,
+    CaptureNamed,
+  )
+where
+
+import Control.Monad ((<=<))
+import Data.Aeson (FromJSON, parseJSON)
+import GDP (Defn, defn, type (~~))
+import Servant (Capture, FromHttpApiData, parseUrlPiece)
+
+-- | Capture a value from the url path.
+type CaptureNamed a = Capture "named input" a
+
+newtype ApiName0 = ApiName0 Defn
+
+type role ApiName0
+
+instance ApiName ApiName0 where
+  doDef = defn
+
+newtype ApiName1 = ApiName1 Defn
+
+type role ApiName1
+
+instance ApiName ApiName1 where
+  doDef = defn
+
+newtype ApiName2 = ApiName2 Defn
+
+type role ApiName2
+
+instance ApiName ApiName2 where
+  doDef = defn
+
+newtype ApiName3 = ApiName3 Defn
+
+type role ApiName3
+
+instance ApiName ApiName3 where
+  doDef = defn
+
+newtype ApiName4 = ApiName4 Defn
+
+type role ApiName4
+
+instance ApiName ApiName4 where
+  doDef = defn
+
+newtype ApiName5 = ApiName5 Defn
+
+type role ApiName5
+
+instance ApiName ApiName5 where
+  doDef = defn
+
+newtype ApiName6 = ApiName6 Defn
+
+type role ApiName6
+
+instance ApiName ApiName6 where
+  doDef = defn
+
+newtype ApiName7 = ApiName7 Defn
+
+type role ApiName7
+
+instance ApiName ApiName7 where
+  doDef = defn
+
+newtype ApiName8 = ApiName8 Defn
+
+type role ApiName8
+
+instance ApiName ApiName8 where
+  doDef = defn
+
+newtype ApiName9 = ApiName9 Defn
+
+type role ApiName9
+
+instance ApiName ApiName9 where
+  doDef = defn
+
+newtype ApiName10 = ApiName10 Defn
+
+type role ApiName10
+
+instance ApiName ApiName10 where
+  doDef = defn
+
+newtype ApiName11 = ApiName11 Defn
+
+type role ApiName11
+
+instance ApiName ApiName11 where
+  doDef = defn
+
+newtype ApiName12 = ApiName12 Defn
+
+type role ApiName12
+
+instance ApiName ApiName12 where
+  doDef = defn
+
+newtype ApiName13 = ApiName13 Defn
+
+type role ApiName13
+
+instance ApiName ApiName13 where
+  doDef = defn
+
+newtype ApiName14 = ApiName14 Defn
+
+type role ApiName14
+
+instance ApiName ApiName14 where
+  doDef = defn
+
+newtype ApiName15 = ApiName15 Defn
+
+type role ApiName15
+
+instance ApiName ApiName15 where
+  doDef = defn
+
+newtype ApiName16 = ApiName16 Defn
+
+type role ApiName16
+
+instance ApiName ApiName16 where
+  doDef = defn
+
+newtype ApiName17 = ApiName17 Defn
+
+type role ApiName17
+
+instance ApiName ApiName17 where
+  doDef = defn
+
+newtype ApiName18 = ApiName18 Defn
+
+type role ApiName18
+
+instance ApiName ApiName18 where
+  doDef = defn
+
+newtype ApiName19 = ApiName19 Defn
+
+type role ApiName19
+
+instance ApiName ApiName19 where
+  doDef = defn
+
+newtype ApiName20 = ApiName20 Defn
+
+type role ApiName20
+
+instance ApiName ApiName20 where
+  doDef = defn
+
+class ApiName b where
+  doDef :: a -> a ~~ b
+
+instance (ApiName n, FromJSON a) => FromJSON (a ~~ n) where
+  parseJSON =
+    return . doDef <=< parseJSON
+
+instance (ApiName n, FromHttpApiData a) => FromHttpApiData (a ~~ n) where
+  parseUrlPiece t =
+    doDef <$> parseUrlPiece t
diff --git a/src/Servant/GDP/ProveInIsolation.hs b/src/Servant/GDP/ProveInIsolation.hs
new file mode 100644
--- /dev/null
+++ b/src/Servant/GDP/ProveInIsolation.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module Servant.GDP.ProveInIsolation (ProvableInIsolation, proveInIsolation) where
+
+import Data.Text (Text)
+import GDP (Proof, introAnd, introOrL, introOrR, (...), type (&&), type (:::), type (||), type (~~))
+import Servant
+  ( FromHttpApiData,
+    parseUrlPiece,
+  )
+
+-- | Check if property P holds for value a or not.
+-- Is used to parse a value from the request with a required proof
+class ProvableInIsolation a p where
+  proveInIsolation :: a -> Either Text (Proof p)
+
+instance (ProvableInIsolation a p1, ProvableInIsolation a p2) => ProvableInIsolation a (p1 && p2) where
+  proveInIsolation x = do
+    p1 <- proveInIsolation x
+    p2 <- proveInIsolation x
+    return $ introAnd p1 p2
+
+instance (ProvableInIsolation a p1, ProvableInIsolation a p2) => ProvableInIsolation a (p1 || p2) where
+  proveInIsolation x = do
+    case (proveInIsolation x, proveInIsolation x) of
+      (Right p1, _) -> return $ introOrL p1
+      (_, Right p2) -> return $ introOrR p2
+      (Left e1, Left e2) -> Left $ e1 <> e2
+
+instance
+  ( FromHttpApiData (a ~~ n),
+    FromHttpApiData a,
+    ProvableInIsolation (a ~~ n) p
+  ) =>
+  FromHttpApiData (a ~~ n ::: p)
+  where
+  parseUrlPiece t =
+    do
+      (j :: a ~~ n) <- parseUrlPiece t
+      (j ...) <$> proveInIsolation j