diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,4 @@
+## 0.1.0.0
+
+- Initial release
+- `Protocol` data type to define protocol and `runProtocol` to interpret it.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Evgeny Poberezkin (c) 2020
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * 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.
+
+    * Neither the name of Author name here nor the names of other
+      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
+OWNER 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,5 @@
+# protocol
+
+Model distributed system as type-level multi-party protocol.
+
+See [docs on hackage](http://hackage.haskell.org/package/protocol/docs/Control-Protocol.html).
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/protocol.cabal b/protocol.cabal
new file mode 100644
--- /dev/null
+++ b/protocol.cabal
@@ -0,0 +1,46 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.33.0.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 891acf4772c5e0911b5e56fb7dd8b4a457d91866ed95b4a3142d852a9c0b9b2a
+
+name:           protocol
+version:        0.1.0.0
+synopsis:       Model distributed system as type-level multi-party protocol
+description:    This package provides type to model distributed multi-party protocols,
+                ensuring the continuity of the associated resource state transitions on the type level
+                for all protocol commands and scenarios.
+category:       Control, Distributed Computing, Distributed Systems, Protocol
+homepage:       https://github.com/epoberezkin/protocol#readme
+bug-reports:    https://github.com/epoberezkin/protocol/issues
+author:         Evgeny Poberezkin
+maintainer:     evgeny@poberezkin.com
+copyright:      2020 Evgeny Poberezkin
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    CHANGELOG.md
+
+source-repository head
+  type: git
+  location: https://github.com/epoberezkin/protocol
+
+library
+  exposed-modules:
+      Control.Protocol
+      Control.Protocol.Example
+      Control.Protocol.Internal
+  other-modules:
+      Paths_protocol
+  hs-source-dirs:
+      src
+  ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Wunused-type-patterns -Wredundant-constraints -Wincomplete-record-updates -Wincomplete-uni-patterns -Wno-name-shadowing
+  build-depends:
+      base >=4.7 && <5
+    , freer-indexed ==0.1.*
+    , singletons ==2.6.*
+  default-language: Haskell2010
diff --git a/src/Control/Protocol.hs b/src/Control/Protocol.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Protocol.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+
+-- |
+-- Module : Control.Protocol
+-- Copyright : (c) Evgeny Poberezkin
+-- License : BSD3
+--
+-- Maintainer  : evgeny@poberezkin.com
+-- Stability   : experimental
+-- Portability : non-portable
+--
+-- This module provides type 'Protocol' to model distributed multi-party protocols,
+-- ensuring the continuity of the associated resource state transitions on the type level
+-- for all protocol commands and scenarios.
+--
+-- It accepts used-defined data type for protocol commands (GADT of kind 'Command') and
+-- the list of protocol participants to create protocol type.
+--
+-- Command type serves as a single abstract api between all participants - it is defined
+-- to allow decoupling type-level requirements for participants implementations.
+--
+-- Function '(->:)' wraps commands into free parameterized monad (see <https://hackage.haskell.org/package/freer-indexed freer-indexed>)
+-- so that they can be chained into type-aligned scenarios, optionally written using do notation.
+-- These scenarios can be interpreted in any monad using 'runProtocol' function,
+-- e.g. to print protocol description or diagram or to execute system-level integration tests.
+--
+-- See protocol definition and scenario examples in @<./Control-Protocol-Example.html Control.Protocol.Example>@.
+module Control.Protocol
+  ( Command,
+    Protocol,
+    ProtocolCmd,
+    (->:),
+    runProtocol,
+  )
+where
+
+import Control.Protocol.Internal
+import Control.XFreer
+import Data.Kind
+import Data.Singletons
+
+-- | Defines the kind of the command data type used by 'Protocol':
+--
+--     * @party@ - the type (normally enumerable) that defines parties of the protocol (here it is used as a kind). This type should be singletonized.
+--     * @state@ - the kind of the protocol resource state.
+--
+-- The first type-level tuple in command constructors defines the party that sends the command, with the initial and final resource states for that party.
+--
+-- The second tuple defines the party that executes command (e.g., provides some api) with its initial final and states.
+--
+-- See @<./Control-Protocol-Example.html Control.Protocol.Example>@ for command example.
+type Command party state = (party, state, state) -> (party, state, state) -> Type -> Type
+
+-- | Protocol data type that wraps a command and explicitly adds command participants.
+--
+-- Its only constructor that is not exported adds command participants
+-- and combines participant states in type-level list so that they can be chained
+-- in type-aligned sequence of commands:
+--
+-- > ProtocolCmd ::
+-- >   Sing (from :: p) ->
+-- >   Sing (to :: p) ->
+-- >   cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a ->
+-- >   ProtocolCmd cmd ps s (Inj ps (Inj ps s from fs') to ts') a
+--
+-- Here:
+--
+--     * @from@ - type of party that sends the command.
+--     * @to@ - type of party that executes command (e.g., provides some API).
+--
+-- 'Protocol' type synonym should be used to construct this type, and function '(->:)' should be used instead of the constructor.
+data ProtocolCmd (cmd :: Command p k) (parties :: [p]) (s :: [k]) (s' :: [k]) (a :: Type) where
+  ProtocolCmd ::
+    Sing (from :: p) ->
+    Sing (to :: p) ->
+    cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a ->
+    ProtocolCmd cmd ps s (Inj ps (Inj ps s from fs') to ts') a
+
+-- | Type synonym to create protocol data type ('ProtocolCmd' wrapped in 'XFree' - parameterized free monad):
+--
+--     * @cmd@ - user-defined command type constructor that should have the kind 'Command'.
+--     * @parties@ - type-level list of participants - it defines the order of participant states in the combined state of the system described by the protocol.
+type Protocol cmd parties = XFree (ProtocolCmd cmd parties)
+
+infix 6 ->:
+
+-- | Function that wraps command into 'ProtocolCmd' type converted into free parameterized monad.
+(->:) ::
+  -- | party that sends command
+  Sing from ->
+  -- | party that executes command
+  Sing to ->
+  -- | command - its initial states for both parties are projected from system state
+  cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a ->
+  -- | final protocol state injects final states of both participants
+  Protocol cmd ps s (Inj ps (Inj ps s from fs') to ts') a
+(->:) f t c = xfree $ ProtocolCmd f t c
+
+-- | 'runProtocol' interprets protocol scenario in any monad,
+-- using passed 'runCmd' function that interprets individual commands.
+runProtocol ::
+  forall m cmd ps s s' a.
+  Monad m =>
+  -- | function to interpret a command
+  (forall from to b. (Sing (P from) -> Sing (P to) -> cmd from to b -> m b)) ->
+  -- | protocol scenario (see example in @'Control.Protocol.Example.Scenario'@)
+  Protocol cmd ps s s' a ->
+  m a
+runProtocol runCmd = loop
+  where
+    loop :: forall s1 s2 b. Protocol cmd ps s1 s2 b -> m b
+    loop (Pure x) = return x
+    loop (Bind c f) = run c >>= loop . f
+    run :: forall s1 s2 b. ProtocolCmd cmd ps s1 s2 b -> m b
+    run (ProtocolCmd from to cmd) = runCmd from to cmd
diff --git a/src/Control/Protocol/Example.hs b/src/Control/Protocol/Example.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Protocol/Example.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
+
+-- |
+-- Module : Control.Protocol.Example
+-- Copyright : (c) Evgeny Poberezkin
+-- License : BSD3
+--
+-- Maintainer  : evgeny@poberezkin.com
+-- Stability   : experimental
+-- Portability : non-portable
+--
+-- Example command and protocol definition.
+module Control.Protocol.Example
+  ( MyProtocol,
+    MyCommand (..),
+    scenario,
+    Party (..),
+    ChannelState (..),
+  )
+where
+
+import Control.Protocol
+import Control.XMonad.Do
+import Data.Singletons.TH
+import Prelude hiding ((>>), (>>=))
+
+$( singletons
+     [d|
+       data Party = Recipient | Broker | Sender
+         deriving (Show, Eq)
+       |]
+ )
+
+-- | Example type defining the possible resource states, in this case some communication channel.
+data ChannelState
+  = None
+  | Ready
+  | Busy
+  deriving (Show, Eq)
+
+-- | Example command data type of kind @'Command' 'Party' 'ChannelState'@.
+data MyCommand :: Command Party ChannelState where
+  Create :: MyCommand '(Recipient, None, Ready) '(Broker, None, Ready) ()
+  Notify :: MyCommand '(Recipient, Ready, Ready) '(Sender, None, Ready) ()
+  Send :: String -> MyCommand '(Sender, Ready, Ready) '(Broker, Ready, Busy) ()
+  Forward :: MyCommand '(Broker, Busy, Ready) '(Recipient, Ready, Ready) String
+
+-- | Example protocol type.
+type MyProtocol = Protocol MyCommand '[Recipient, Broker, Sender]
+
+r :: Sing Recipient
+r = SRecipient
+
+b :: Sing Broker
+b = SBroker
+
+s :: Sing Sender
+s = SSender
+
+-- | Example protocol scenario.
+--
+-- If you modify this scenario to 'Send' before channel is 'Create'd or
+-- to 'Send' two messages in a row without forwarding them, the scenario will not compile.
+scenario :: String -> MyProtocol '[None, None, None] '[Ready, Ready, Ready] String
+scenario str = do
+  r ->: b $ Create
+  r ->: s $ Notify
+  s ->: b $ Send str
+  -- s ->: b $ Send str
+  b ->: r $ Forward
diff --git a/src/Control/Protocol/Internal.hs b/src/Control/Protocol/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Protocol/Internal.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+
+-- |
+-- Module : Control.Protocol.Internal
+-- Copyright : (c) Evgeny Poberezkin
+-- License : BSD3
+--
+-- Maintainer  : evgeny@poberezkin.com
+-- Stability   : experimental
+-- Portability : non-portable
+--
+-- This module provides type families to combine/extract the individual states of parties
+-- as defined by command constructors into/from the combined system/protocol state defined as type-level list.
+module Control.Protocol.Internal where
+
+import GHC.TypeLits (ErrorMessage (..), TypeError)
+
+-- | Extracts party from command type parameter.
+type family P (partyCmd :: (party, s, s)) where
+  P '(p, _, _) = p
+
+-- | Projects the state of one party from the list of states.
+type family Prj (parties :: [pk]) (state :: [k]) (party :: pk) :: k where
+  Prj (p ': _) (s ': _) p = s
+  Prj (_ ': ps) (_ ': ss) p = Prj ps ss p
+  Prj '[] _ p = TypeError (NoParty p)
+  Prj _ '[] p = TypeError (NoParty p :$$: StateError)
+
+-- | Injects the state of some party into the party's position in the list of states.
+type family Inj (parties :: [pk]) (state :: [k]) (p :: pk) (s' :: k) :: [k] where
+  Inj (p ': _) (_ ': ss) p s' = s' ': ss
+  Inj (_ ': ps) (s ': ss) p s' = s ': Inj ps ss p s'
+  Inj '[] _ p _ = TypeError (NoParty p)
+  Inj _ '[] p _ = TypeError (NoParty p :$$: StateError)
+
+type NoParty p = Text "Party " :<>: ShowType p :<>: Text " is not found."
+
+type StateError = Text "Specified fewer protocol states than parties."
