diff --git a/Src/Command.hs b/Src/Command.hs
index 33744d2..49e784d 100644
--- a/Src/Command.hs
+++ b/Src/Command.hs
@@ -8,10 +8,14 @@ import Control.Monad.Reader
 import Control.Monad.State
 
 import Data.Bifunctor (bimap, first)
+import Data.Char (isSpace)
+import Data.Map (Map)
 import qualified Data.Map as Map
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, catMaybes)
 import Data.Traversable (for)
 import Data.Foldable (asum)
+import qualified Data.Set as Set
+import Data.These (These(..), mergeThese)
 
 import Actor
 import Actor.Display ()
@@ -32,19 +36,23 @@ import Machine.Trace (Shots)
 import Options
 import Parse
 import Pretty
+import Rules
 import Syntax
 import Term.Base
 import Unelaboration.Monad (Unelab(..), Naming, subunelab, withEnv)
 import Unelaboration (initDAEnv, declareChannel)
 import Location
-
-import Data.Char (isSpace)
 import Operator
 import Thin
 import Operator.Eval (HeadUpData' (..))
 import Hide (Hide(..))
 import Scope (Scope(..))
 
+import Utils
+import Data.Either (partitionEithers)
+import Data.List (sort, sortBy)
+import Data.Function (on)
+
 type family DEFNPROTOCOL (ph :: Phase) :: *
 type instance DEFNPROTOCOL Concrete = ()
 type instance DEFNPROTOCOL Abstract = AProtocol
@@ -76,6 +84,8 @@ data COMMAND (ph :: Phase)
   | Trace [MachineStep]
   | OpBlock [OPENTRY ph]
   | Typecheck (TERM ph) (SEMANTICSDESC ph)
+  | DeclJudgementForm (JUDGEMENTFORM ph)
+  | DeclRule (RULE ph)
 
 deriving instance
   ( Show (JUDGEMENTNAME ph)
@@ -99,6 +109,8 @@ deriving instance
   , Show (DEFNPROTOCOL ph)
   , Show (LOOKEDUP ph)
   , Show (DEFNOP ph)
+  , Show (JUDGEMENTFORM ph)
+  , Show (RULE ph)
   , Show (GUARD ph)) =>
   Show (COMMAND ph)
 
@@ -127,6 +139,13 @@ instance Display AProtocol where
 instance Pretty CStatement where
   pretty (Statement jd vars) = hsep $ pretty jd : (pretty <$> vars)
 
+instance Pretty (PLACE Concrete) where
+  pretty (v, CitizenPlace) = pretty v
+  pretty (v, SubjectPlace (WithRange _ syntaxcat) (semanticsdesc, _)) =
+    parens $ hsep $ [ pretty v, ":", pretty syntaxcat ]
+      ++ (("=>" <+> pretty semanticsdesc)
+          <$ guard (At unknown syntaxcat /= semanticsdesc))
+
 instance Pretty CCommand where
   pretty = let prettyCds cds = collapse (BracesList $ pretty <$> cds) in \case
     DeclJudge em jd p -> hsep [pretty em <> pretty jd, colon, pretty p]
@@ -140,6 +159,9 @@ instance Pretty CCommand where
                                                      , prettyCds posts]
     Go a -> keyword "exec" <+> pretty a
     Trace ts -> keyword "trace" <+> collapse (BracesList $ map pretty ts)
+    DeclJudgementForm j -> keyword "judgementform" <+> collapse (BracesList $ pretty <$> jpreconds j)
+                        <+> hsep (pretty (jname j) : map pretty (jplaces j))
+                        <+> collapse (BracesList $ either pretty pretty <$> jpostconds j)
     Typecheck t ty -> keyword "typecheck" <+> pretty t <+> ":" <+> pretty ty
 
 instance Unelab ACommand where
@@ -196,6 +218,8 @@ pcommand
                     <* pspc <*> pconditions
   <|> Go <$ plit "exec" <* pspc <*> pACT
   <|> Trace <$ plit "trace" <*> pcurlies (psep (ppunc ",") pmachinestep)
+  <|> DeclJudgementForm <$> pjudgementform
+  <|> DeclRule <$> prule
   <|> OpBlock <$ plit "operator"
               <*> pcurlies (psep (ppunc ";") (DeclOp <$> panoperator <|> DefnOp <$> pdefnop))
   <|> Typecheck <$ plit "typecheck" <* pspc <*> pTM <* ppunc ":" <*> pTM
@@ -278,6 +302,7 @@ sdeclOp (AnOperator (objBinder, objDescPat) (WithRange r opname) paramDescs retD
     (paramDescs, ds) <- sparamdescs paramDescs
     retDesc <- local (setDecls ds) $ sty retDesc
     pure $ AnOperator (objName, descPat) opname paramDescs retDesc
+  -- Process the rest of the declarations, in the original context
   local (addOperator op) $ (op,) <$> asks globals
 
 scommand :: CCommand -> Elab (ACommand, Globals)
@@ -321,16 +346,136 @@ scommand = \case
     (ContractStack pres (stk, lhs, rhs) posts,) <$> asks globals
   Go a -> during ExecElaboration $ (,) . Go <$> local (setElabMode Execution) (sact a) <*> asks globals
   Trace ts -> (Trace ts,) <$> asks globals
+  DeclJudgementForm j -> do
+    (j , gs) <- sjudgementform j
+    pure (DeclJudgementForm j, gs)
   Typecheck t ty -> do
     ty <- sty ty
     t <- stm DontLog ty t
     g <- asks globals
     pure (Typecheck t ty, g)
-
-  -- Sig S \x.T - 'fst ~> S
-  -- (p : Sig S \x.T) - 'snd ~> {x=[ p - 'fst ]}T
   OpBlock ops -> first OpBlock <$> sopBlock ops
 
+checkCompatiblePlaces :: [PLACE Concrete] ->
+                    [(Variable, ASemanticsDesc)] ->
+                    [(Variable, ASemanticsDesc)] ->
+                    Elab ()
+checkCompatiblePlaces places inputs outputs = do
+  -- Make sure subject protocol can be found unambiguously
+  let names = map fst places
+  let citizenNames = [x | (x, CitizenPlace) <- places]
+  let inputNames = map fst inputs
+  let outputNames = map fst outputs
+  whenLeft (allUnique names) $ \ a -> throwComplaint a $ DuplicatedPlace a
+  inputNamesSet <- case allUnique inputNames of
+    Left a -> throwComplaint a $ DuplicatedInput a
+    Right as -> pure as
+  outputNamesSet <- case allUnique outputNames of
+    Left a -> throwComplaint a $ DuplicatedOutput a
+    Right as -> pure as
+  whenCons (Set.toList (Set.intersection inputNamesSet outputNamesSet)) $ \ a _ ->
+    throwComplaint a $ BothInputOutput a
+  whenCons (mismatch citizenNames inputNames outputNames) $ \ (v, m) _ ->
+    throwComplaint v (ProtocolCitizenSubjectMismatch v m)
+  where
+    mismatch :: [Variable]
+             -> [Variable]
+             -> [Variable]
+             -> [(Variable, Mode ())]
+    mismatch cs is os =
+      catMaybes $ alignWith check (sort cs)
+                $ sortBy (compare `on` fst)
+                $ map (, Input) is ++ map (, Output) os
+
+    check :: These Variable (Variable, Mode ()) -> Maybe (Variable, Mode ())
+    check (These a b) = (a, Subject ()) <$ guard (a /= fst b)
+    check t = Just (mergeThese const (first (, Subject ()) t))
+
+
+{-
+Do not use operators to compute citizens from subjects.
+Rather, transmit glued subject-citizen pairs,
+when matching a subject, glue metavars to pattern vars
+then use s => c clauses ub rules to constrain the citizen
+the parent sent with the subject syntax.
+-}
+
+sjudgementform :: JUDGEMENTFORM Concrete
+               -> Elab (JUDGEMENTFORM Abstract, Globals)
+sjudgementform JudgementForm{..} = during (JudgementFormElaboration jname) $ do
+  inputs <- concat <$> traverse subjects jpreconds  -- TODO: should really be the closure of this info
+  let (outputs, operators) = partitionEithers jpostconds
+  outputs <- concat <$> traverse subjects outputs
+  checkCompatiblePlaces jplaces inputs outputs
+  (ps, subjectKinds, _) <- citizenJudgements Map.empty inputs outputs jplaces
+  let protocol = Protocol ps
+  jname <- isFresh jname
+  local (declare (Used jname) (AJudgement jextractmode protocol)) $ do
+    (operators, gs) <- sopBlock . map DeclOp =<< traverse (kindify subjectKinds) operators
+    pure ((jextractmode, jname, protocol), gs)
+
+
+  where
+    subjects :: JUDGEMENT Concrete -> Elab [(Variable, ASemanticsDesc)]
+    subjects (Judgement r name fms) = do
+      IsJudgement{..} <- isJudgement name
+      xs <- case halfZip (getProtocol judgementProtocol) fms of
+        Just xs -> pure xs
+        Nothing -> throwComplaint r $ JudgementWrongArity judgementName judgementProtocol fms
+      let ys = [ (fm, sem) | ((Subject _, sem), fm) <- xs ]
+      forM ys $ \case
+        -- TODO: should use something like `isSendableSubject`
+        (CFormula (These _ (Var r x)), sem) -> pure (x, sem)
+        (x, _) -> throwComplaint r $ UnexpectedNonSubject x
+
+    citizenJudgements :: Map Variable RawP
+                      -> [(Variable, ASemanticsDesc)]
+                      -> [(Variable, ASemanticsDesc)]
+                      -> [CPlace]
+                      -> Elab ( [AProtocolEntry]
+                              , Map Variable RawP
+                              , Decls )
+    citizenJudgements mp inputs outputs [] = ([], mp,) <$> asks declarations
+    citizenJudgements mp inputs outputs ((name, place) : plcs) = case place of
+      CitizenPlace -> do
+        bd <- Used <$> isFresh name
+        th <- asks (ones . scopeSize . objVars)
+        case (lookup name inputs, lookup name outputs) of
+          (Just isem, Nothing) -> do
+            (_, asot) <- thickenedASOT (getRange name) th isem
+            (ps, mp, ds) <- local (declare bd (ActVar IsNotSubject asot)) $
+              citizenJudgements mp inputs outputs plcs
+            pure ((Input, isem) : ps, mp, ds)
+          (Nothing, Just osem) -> do
+            (_, asot) <- thickenedASOT (getRange name) th osem
+            (ps, mp, ds) <- local (declare bd (ActVar IsNotSubject asot)) $
+              citizenJudgements mp inputs outputs plcs
+            pure ((Output, osem) : ps, mp, ds)
+          _  -> error "Impossible in citizenJudgement"
+
+      SubjectPlace (WithRange r rsyn) (sem, msempat) -> do
+        syndecls <- gets (Map.keys . syntaxCats)
+        unless (rsyn `elem` syndecls) $
+            throwComplaint r $ InvalidSubjectSyntaxCat rsyn syndecls
+        syn <- satom rsyn
+        -- TODO: we use underScore here if the type is not a valid pattern, eg a stuck neutral. It would be good to do better.
+        mp <- pure (Map.insert name (fromMaybe (UnderscoreP unknown) msempat) mp)
+        (ps, mp, ds) <- citizenJudgements mp inputs outputs plcs
+        sem <- local (setDecls ds) $ sty sem
+        pure ((Subject syn, sem) : ps, mp, ds)
+
+    kindify :: Map Variable RawP -> CAnOperator -> Elab CAnOperator
+    kindify m op
+      | (Used x, pat) <- objDesc op
+      , Just sempat <- Map.lookup x m
+      = do
+          case pat of
+            UnderscoreP _ -> pure ()
+            _ -> when (pat /= sempat) $ throwComplaint pat $ MismatchedObjectPattern (theValue (opName op)) pat sempat
+          pure (op { objDesc = (Used x, sempat) })
+      | otherwise = throwComplaint (fst $ objDesc op)
+                  $ MalformedPostOperator (theValue (opName op)) (Map.keys m)
+
 sopBlock :: [OPENTRY Concrete] -> Elab ([OPENTRY Abstract], Globals)
 sopBlock [] = ([],) <$> asks globals
 sopBlock (DefnOp (rp, opelims@((rpty,_,_):_), rhs) : rest) = do
diff --git a/Src/Concrete/Base.hs b/Src/Concrete/Base.hs
index 852147b..be2b5d4 100644
--- a/Src/Concrete/Base.hs
+++ b/Src/Concrete/Base.hs
@@ -218,13 +218,15 @@ data ExtractMode
   deriving (Show, Eq)
 
 data Keyword
-  = KwSyntax | KwExec | KwTrace
+  = KwSyntax | KwRule | KwJudgementForm | KwExec | KwTrace
   | KwLet | KwCase | KwLookup | KwCompare
   | KwBREAK | KwPRINT | KwPRINTF
   deriving (Enum, Bounded)
 
 instance Show Keyword where
   show KwSyntax = "syntax"
+  show KwRule = "rule"
+  show KwJudgementForm = "judgementform"
   show KwExec = "exec"
   show KwTrace = "trace"
   show KwLet = "let"
diff --git a/Src/Elaboration.hs b/Src/Elaboration.hs
index c0fde82..fee9fb8 100644
--- a/Src/Elaboration.hs
+++ b/Src/Elaboration.hs
@@ -38,10 +38,11 @@ import Control.Applicative ((<|>))
 import Operator
 import Operator.Eval
 import Semantics
--- import Debug.Trace (traceShow, traceShowId, trace)
 import Data.Bifunctor (bimap)
 import GHC.Stack.Types (HasCallStack)
 
+-- import Debug.Trace (traceShow, traceShowId, trace)
+
 type CPattern = PATTERN Concrete
 type APattern = PATTERN Abstract
 
@@ -518,7 +519,7 @@ itms :: Range -> String -> Usage
         --
      -> Elab (ASemanticsDesc -- Instantiated return type
              , [ACTm])       -- Elaborated parameters
-itms r op usage [] [] rdesc = (, []) <$> instantiateDesc r rdesc
+itms r op usage [] [] rdesc = (, []) <$> (instantiateDesc r rdesc)
 itms r op usage ((binder, sot):bs) (rp:rps) rdesc = do
   (ovs :=> desc) <- instantiateSOT (getRange rp) sot
   (p, dat) <- sparam usage binder B0 (discharge ovs desc) rp
diff --git a/Src/Elaboration/Monad.hs b/Src/Elaboration/Monad.hs
index 613322b..8076d54 100644
--- a/Src/Elaboration/Monad.hs
+++ b/Src/Elaboration/Monad.hs
@@ -21,6 +21,7 @@ import Thin
 import Term.Base
 import Utils
 import Operator
+import Rules
 import Info
 import Pattern
 import Hide
@@ -309,10 +310,19 @@ declareObjVar :: ( {- x :: -} String
               -> Context {- gamma, x :: S -}
 declareObjVar (x, sem) ctx =
     -- We store semantics descs ready to be deployed at use sites
-    let scp = getObjVars (objVars ctx) :< ObjVar x sem in
+    let scp = getObjVars (objVars ctx) :< ObjVar x sem
+        dat = headUpData ctx
+    in
     ctx { objVars = ObjVars (fmap weak <$> scp)
         , binderHints = fmap weak <$> binderHints ctx
+        , headUpData = dat { huEnv = weakenEnvWith x (huEnv dat) }
         }
+  where
+    -- we extend the global scope so that mangleActors will bring the
+    -- operator types into local scope during instantiation
+    weakenEnvWith :: String -> Env' m -> Env' m
+    weakenEnvWith x env = env { globalScope = globalScope env :< x}
+
 
 -- Careful! The new ovs better be a valid scope
 -- i.e. all the objvars mentioned in the SemanticsDesc of
@@ -505,6 +515,17 @@ data Complaint
   | ProtocolsNotDual AProtocol AProtocol
   | IncompatibleModes AProtocolEntry AProtocolEntry
   | WrongDirection AProtocolEntry Ordering AProtocolEntry
+  -- judgementforms
+  | JudgementWrongArity JudgementName AProtocol [CFormula]
+  | UnexpectedNonSubject CFormula
+  | DuplicatedPlace Variable
+  | DuplicatedInput Variable
+  | DuplicatedOutput Variable
+  | BothInputOutput Variable
+  | ProtocolCitizenSubjectMismatch Variable (Mode ())
+  | MalformedPostOperator String [Variable]
+  | MismatchedObjectPattern String RawP RawP
+  | InvalidSubjectSyntaxCat SyntaxCat [SyntaxCat]
   -- syntaxes
   | AlreadyDeclaredSyntaxCat SyntaxCat
   -- syntaxdesc validation
diff --git a/Src/Elaboration/Pretty.hs b/Src/Elaboration/Pretty.hs
index 064ff2a..10cd3d8 100644
--- a/Src/Elaboration/Pretty.hs
+++ b/Src/Elaboration/Pretty.hs
@@ -6,7 +6,7 @@ import Data.Foldable
 
 import ANSI hiding (withANSI)
 import Actor (ActorMeta'(..), ActorMeta, Channel(..), Stack(..), AProtocol)
-import Concrete.Base (Binder (..), PROTOCOL(Protocol))
+import Concrete.Base (Binder (..), PROTOCOL(Protocol), Mode (..))
 import Concrete.Pretty()
 import Elaboration.Monad
 import Location
@@ -156,6 +156,32 @@ instance Pretty (WithRange Complaint) where
     WrongDirection m1 dir m2 -> hsep ["Wrong direction", pretty (show dir)
                                      , "between", pretty (WithVarNames B0 <$> m1)
                                      , "and", pretty (WithVarNames B0 <$> m2)]
+    -- judgementforms
+    JudgementWrongArity name (Protocol protocol) fms ->
+        let applied = (if length protocol > length fms then "under" else "over") <> "-applied" in
+        hsep ["Judgement", pretty name, applied]
+    UnexpectedNonSubject fm -> hsep ["Unexpected non-subject", pretty fm]
+    DuplicatedPlace v -> hsep [pretty v, "is a duplicated place" ]
+    DuplicatedInput v -> hsep [pretty v, "is a duplicated input"]
+    DuplicatedOutput v -> hsep [pretty v, "is a duplicated output"]
+    BothInputOutput v -> hsep [pretty v, "is both an input and an output"]
+    ProtocolCitizenSubjectMismatch v m ->
+      let (seen, unseen) = case m of
+            Input -> ("an input", "not as a subject")
+            Subject{} -> ("a subject", "neither as an input nor an output")
+            Output -> ("an output", "not as a subject")
+      in hsep ["Found", pretty v, "as", seen, "but", unseen ]
+    MalformedPostOperator op cands ->
+      let message = case cands of [x] -> "the subject"
+                                  _   -> "a subject among" in
+      hsep $ ["Malformed operator", pretty op <> "; expected it to act on", message] ++ punctuate ", " (map pretty cands)
+    MismatchedObjectPattern op got expected ->
+      vcat [ hsep ["Mismatched object type pattern in operator declaration of ", pretty op <> "."]
+           , hsep ["Expected", pretty expected, "but got", pretty got]
+           ]
+    InvalidSubjectSyntaxCat got known -> vcat [hsep ["Invalid subject syntax category", pretty got]
+                                              , hsep ("Expected one among" : punctuate ", " (map pretty known))
+                                              ]
     -- syntaxes
     AlreadyDeclaredSyntaxCat x -> hsep ["The syntactic category", pretty x, "is already defined"]
 
@@ -166,7 +192,8 @@ instance Pretty (WithRange Complaint) where
       hsep [ "Incompatible semantics descriptions, expected"
            , prettyPrec 1 desc
            , "but got"
-           , prettyPrec 1 desc']
+           , prettyPrec 1 desc'
+           ]
     IncompatibleSyntaxInfos info1 info2 ->
       hsep ["Syntax infos" , pretty (WithVarNames B0 <$> info1)
            , "and", pretty (WithVarNames B0 <$> info2)
diff --git a/Src/Operator.hs b/Src/Operator.hs
index b401560..8997409 100644
--- a/Src/Operator.hs
+++ b/Src/Operator.hs
@@ -184,23 +184,22 @@ poperator ph =
   (,[]) <$> pwithRange patom
   <|> (,) <$ pch (== '[') <* pspc <*> pwithRange patom <*> many (id <$ pspc <*> ph) <* pspc <* pch (== ']')
 
-pBinders :: Parser (a, b) -> Parser (a, ([(Raw, Variable)], b))
-pBinders p = fmap . (,) <$> many ((,) <$> pTM <* ppunc "\\" <*> pvariable <* pspc <* pch ('.' ==)) <*> p
+pBinders :: Parser a -> Parser ([(Raw, Variable)], a)
+pBinders p = (,) <$> many ((,) <$> pTM <* ppunc "\\" <*> pvariable <* ppunc ".") <*> p
 
 panoperator :: Parser CAnOperator
 panoperator = do
   obj <- pmaybeNamed ppat (withRange $ pure $ UnderscoreP unknown)
   ppunc "-"
-  (opname, params) <- poperator $ pBinders (pmaybeNamed psemanticsdecl pfail)
+  (opname, params) <- poperator $ pmaybeNamed (pBinders psemanticsdecl) pfail
   ppunc ":"
   AnOperator obj opname (fmap (fmap $ uncurry CSOT) params) <$> psemanticsdecl
- where
-  pmaybeNamed :: Parser a -- if binder
+  where
+    pmaybeNamed :: Parser a -- if binder
               -> Parser a -- if no binder
-              -> Parser (Binder (ACTORVAR Concrete), a)
-  pmaybeNamed p q
-    = pparens ((,) <$> pbinder <* ppunc ":" <*> p)
-    <|> ((,) . Used <$> pvariable <*> q)
+              -> Parser (Binder Variable, a)
+    pmaybeNamed p q = pparens ((,) <$> pbinder <* ppunc ":" <*> p)
+                 <|> ((,) . Used <$> pvariable <*> q)
 
 instance Pretty CAnOperator where
   pretty (AnOperator obj (WithRange _ opName) paramsDesc retDesc) =
diff --git a/Src/Operator/Eval.hs b/Src/Operator/Eval.hs
index 0c2e0aa..085f90e 100644
--- a/Src/Operator/Eval.hs
+++ b/Src/Operator/Eval.hs
@@ -32,7 +32,7 @@ data HeadUpData' m = forall i d. HeadUpData
   , metaStore :: StoreF i d
   , huOptions :: Options
   , huEnv :: Env' m
-  , whatIs :: m -> Maybe (Term' m)
+  , whatIs :: m -> Maybe (Term' m) -- how to look up meta variables
   }
 
 instance Show (HeadUpData' m) where
diff --git a/Src/Rules.hs b/Src/Rules.hs
new file mode 100644
index 0000000..7f87e10
--- /dev/null
+++ b/Src/Rules.hs
@@ -0,0 +1,159 @@
+{-# LANGUAGE UndecidableInstances,  OverloadedStrings #-}
+module Rules where
+
+import Control.Applicative
+
+import Data.These
+import Data.Maybe
+
+import Actor
+import Scope
+import Concrete.Base
+import Operator (DEFNOP, ANOPERATOR, pdefnop, panoperator)
+import Term.Base
+
+import Parse
+import Location
+import Concrete.Parse
+import Syntax (psyntaxcat)
+import Pretty
+
+type family FORMULA (ph :: Phase) :: *
+type instance FORMULA Concrete = CFormula
+type instance FORMULA Abstract = AFormula
+
+data CFormula
+  = CFormula (These RawP Raw) -- we don't know if we need a pattern or term yet
+  | CCitizen RawP Raw  -- (pat => term)
+  deriving (Show)
+
+data AFormula
+  = Coming Pat
+  | Going  Term
+  | Citizen Pat Term -- pat => term
+  deriving (Show)
+
+-- _=>_ should be a constructor of FORMULA?
+-- a raw formula is an expression (and we might make it into a pattern later)
+data JUDGEMENT (ph :: Phase)
+  = Judgement Range (JUDGEMENTNAME ph) [FORMULA ph]
+
+instance HasSetRange (JUDGEMENT ph) where
+  setRange r (Judgement _ n fms) = Judgement r n fms
+
+data PREMISE (ph :: Phase)
+  = Premise (JUDGEMENT ph)
+  | Binding Range (Scope (Binder Variable) (PREMISE ph))
+  | Hypothetical (JUDGEMENT ph) (PREMISE ph)
+  | Constraint (TERM ph) (TERM ph)
+
+data RULE (ph :: Phase) = RULE
+  { premises :: [PREMISE ph]
+  , conclusion :: JUDGEMENT ph
+  , operatorDefs :: [DEFNOP ph]
+  }
+
+type PLACE (ph :: Phase) = (Variable, PLACEKIND ph)
+type CPlace = PLACE Concrete
+
+
+data PLACEKIND (ph :: Phase)
+  = CitizenPlace
+  | SubjectPlace (SYNTAXCAT ph) (SEMANTICSDESC ph, Maybe (PATTERN ph))
+
+mkSubjectPlace :: SYNTAXCAT Concrete
+               -> Maybe (SEMANTICSDESC Concrete, Maybe (PATTERN Concrete))
+               -> PLACEKIND Concrete
+mkSubjectPlace syn
+  = SubjectPlace syn
+  . fromMaybe ( At (getRange syn) (theValue syn)
+              , Just (AtP (getRange syn) (theValue syn)))
+
+data CJudgementForm = JudgementForm
+  { jrange :: Range
+  , jpreconds :: [JUDGEMENT Concrete]
+  , jextractmode :: ExtractMode
+  , jname :: JUDGEMENTNAME Concrete
+  , jplaces :: [PLACE Concrete]
+  , jpostconds :: [Either (JUDGEMENT Concrete) (ANOPERATOR Concrete)]
+  }
+  deriving Show
+
+type AJudgementForm = (ExtractMode, String, AProtocol)
+
+instance HasSetRange CJudgementForm where
+  setRange r (JudgementForm _ a b c d e) = JudgementForm r a b c d e
+
+
+type family JUDGEMENTFORM (ph :: Phase) :: *
+type instance JUDGEMENTFORM Concrete = CJudgementForm
+type instance JUDGEMENTFORM Abstract = AJudgementForm
+
+
+deriving instance
+  ( Show (JUDGEMENTNAME ph)
+  , Show (FORMULA ph)) =>
+  Show (JUDGEMENT ph)
+
+deriving instance
+  ( Show (JUDGEMENT ph)
+  , Show (TERM ph)) =>
+  Show (PREMISE ph)
+
+deriving instance
+  ( Show (PREMISE ph)
+  , Show (JUDGEMENT ph)
+  , Show (DEFNOP ph)) =>
+  Show (RULE ph)
+
+deriving instance
+  ( Show (SYNTAXCAT ph)
+  , Show (SEMANTICSDESC ph)
+  , Show (PATTERN ph)) =>
+  Show (PLACEKIND ph)
+
+pformula :: Parser CFormula
+pformula = pcitizen
+         <|> CFormula <$> pthese ppat ptm
+  where
+    pcitizen = pparens pcitizen
+             <|> CCitizen <$> ppat <* ppunc "=>" <*> ptm
+
+pjudgement :: Parser (JUDGEMENT Concrete)
+pjudgement = withRange $ Judgement unknown <$> pvariable <*> many (id <$ pspc <*> pformula)
+
+ppremise :: Parser (PREMISE Concrete)
+ppremise = pscoped Binding pbinder ppremise
+        <|> (pjudgement >>=
+               \ j -> ((Hypothetical j <$ ppunc "|-" <*> ppremise) <|> (pure $ Premise j)))
+        <|> Constraint <$> ptm <* ppunc "=" <*> ptm
+
+prule :: Parser (RULE Concrete)
+prule = RULE <$ pkeyword KwRule <*> pcurlies (psep (ppunc ";") ppremise)
+      <* pspc <*> pjudgement <*> pcurlies (psep (ppunc ";") pdefnop)
+
+psubjectSem :: Parser (SEMANTICSDESC Concrete, Maybe (PATTERN Concrete))
+psubjectSem = pthese pTM ppat >>= \case
+  This sem -> pure (sem, Nothing)
+  These sem pat -> pure (sem, Just pat)
+  That pat -> pfail
+
+pplace :: Parser (PLACE Concrete)
+pplace = (,CitizenPlace) <$> pvariable <|> pparens ((,) <$> pvariable <* ppunc ":"
+                        <*> (mkSubjectPlace <$> psyntaxcat
+                        <*> optional (id <$ ppunc "=>" <*> psubjectSem)))
+
+pjudgementform :: Parser CJudgementForm
+pjudgementform = withRange $ JudgementForm unknown
+  <$ pkeyword KwJudgementForm
+  <*> pcurlies (psep (ppunc ";") pjudgement)
+  <* pspc <*> pextractmode <*> pvariable
+  <* pspc <*> psep pspc pplace
+  <*> pcurlies (psep (ppunc ";") (Left <$> pjudgement <|> Right <$> panoperator))
+
+instance Pretty (JUDGEMENT Concrete) where
+  pretty (Judgement _ jname fms) = hsep (pretty jname:map pretty fms)
+
+instance Pretty CFormula where
+  pretty (CFormula fm) = mergeTheseWith pretty pretty const fm
+  pretty (CCitizen pat tm) = hsep [pretty pat, "=>", pretty tm]
diff --git a/emacs/typos.el b/emacs/typos.el
index 67a42f5..14acf63 100644
--- a/emacs/typos.el
+++ b/emacs/typos.el
@@ -7,6 +7,7 @@
                         "break" "unify" "send" "recv" "move"
                         "case" "let"
                         "Atom" "AtomBar" "Wildcard" "EnumOrTag" "Enum" "Tag" "Cons" "Nil" "NilOrCons" "Fix" "Bind"
+                        "Syntax" "Semantics"
                         "BREAK" "PRINT" "PRINTF"))
 (setq typos-operators '("@" "!" "$" "?" "~" "#"))
 (setq typos-symbols   '("|-" "|" "<->" "->" "~>" ";" "=>" "=" "{" "}"))
diff --git a/examples/stlcRules.act b/examples/stlcRules.act
new file mode 100644
index 0000000..ca02b85
--- /dev/null
+++ b/examples/stlcRules.act
@@ -0,0 +1,129 @@
+------------------------------------------------------------------------------
+-- Datatypes
+
+syntax
+  { 'Type = ['EnumOrTag  ['Nat]
+                         [['Arr 'Type 'Type]]
+            ]
+  }
+
+syntax
+  { 'Check = ['Tag [ ['Lam ['Bind 'Synth 'Check]]
+                     ['Emb 'Synth]
+             ]]
+  ; 'Synth = ['Tag [ ['Ann 'Check 'Type]
+                     ['App 'Synth 'Check]
+             ]]
+  }
+
+-- this is in 'Semantics, or so we declare
+syntax -- we're calling it not-'Nat on purpose
+  { 'Natural = ['EnumOrTag ['Zero]
+                           [['Succ 'Natural]]
+               ]
+  }
+
+------------------------------------------------------------------------------
+-- Judgement forms and their contracts
+
+-- Something that looks like "Z : A => B" says
+-- Z is an A when it's a subject, and a B when it becomes a citizen
+
+judgementform
+  {} -- no precondition
+  type (T : 'Type) -- no '=> B' means the citizen version is the same
+  {T - 'Value : 'Semantics} -- postcondition: a 'Value operator becomes available
+
+judgementform
+  {type T} -- precondition: T has been judged to be a type
+  check T (t : 'Check => T - 'Value) -- once validated, t becomes its denotational semantics
+  {} -- no postcondition
+
+judgementform
+  {}
+  synth (e : 'Synth => S - 'Value) S
+  {type S} -- postcondition: the output will be a valid type
+
+
+-- Open question in the above: will it always be the subject that's fed to an operator?
+-- Note: the "T - 'Value" is in 'Semantics and that T is the citizen, not the subject
+
+-- {} myCtxt |- x -> T {synth x T}
+
+rule
+  {}
+  --------------------------- (nat)
+  type 'Nat
+  {'Nat - 'Value ~> 'Natural}
+
+rule
+  {type S; type T}
+  ------------------------------------------------------------ (arr)
+  type ['Arr S T]
+  {['Arr S T] - 'Value ~> ['Pi (S - 'Value) \_. (T - 'Value)]}
+
+-- Invariant: the subject in a premise is always something with a name
+-- payoff - the name BECOMES the name of the citizen
+
+rule
+  { \ x . synth x S |- check T body }
+  -- x is a hypothetical inhabitant of S - 'Value
+  -- hypothetical judgement with fresh x, assuming `synth x S`
+  -- (note hypothetical judgements have patterns in input and subject
+  --  positions, and expressions in output positions)
+  -----------------------------------------------
+  check ~['Arr S T] (['Lam \x. body] => \x. body)
+  -- ~['Arr S T] means to not match, but to constrain instead
+  {}
+-- Could equivalently be written without deliberate capture of x:
+--  { \ y . synth y S |- check T {x=y}body }
+-- note that if we use the above, then we'd expect to capture a y in S - 'Value in body the citizen
+-- the elaborator-check that body is used fully generally in the premise subject
+-- needs to return the variables that are in scope for body the citizen
+
+rule
+  { synth e S
+  ; S = T -- by the magic of STLC, things are first-order, this is just unification
+  }
+  ---------------------
+  check T (['Emb e] => e)
+  {}
+
+-- first arg is a (subject) pattern position
+-- 2nd argument is in output position & we give the citizen T
+--   Note to selves: holy readability issues!
+
+rule
+  { type T
+  ; check T t
+  }
+  synth (['Ann t T] => t) T
+  {}
+
+rule
+  { synth f ~['Arr S T]
+  ; check S s
+  }
+  synth (['App f s] => (f -['app s])) T     -- assuming citizen 'f' is meta-level function
+  -- irrefutable because of no overloading of application (in STLC)
+  {}
+
+------------------------------------------------------------------------------
+
+
+------------------------------------------------------------------------------
+-- Examples
+{-
+exec check@p. p! ['Arr 'Nat ['Arr 'Nat 'Nat]].
+              p! ['Lam \z. ['Lam \_. ['Emb z]]].
+exec check@p. p! ['Arr 'Nat 'Nat].
+              p! ['Lam \z. ['Emb z]].
+
+
+exec check@p.
+   p! ['Arr 'Nat 'Nat].
+   p! ['Lam \z. ['Emb
+         ['App ['Ann ['Lam \w. ['Emb w]] ['Arr 'Nat 'Nat]]
+         ['Emb z]]]].
+   PRINTF "Victory!".
+-}
diff --git a/syntax.txt b/syntax.txt
new file mode 100644
index 0000000..6aa885a
--- /dev/null
+++ b/syntax.txt
@@ -0,0 +1,49 @@
+__________________________________________________________
+                 |
+  telescopes in  |  syntax (^^^ indicates optional parts)
+_________________|________________________________________
+                 |
+  protocols      |  [?!$](x,y,z:type).
+                 |       ^^^^^^^    ^
+_________________|________________________________________
+                 |
+  sot            |  ^(x,y,z:type).sot
+                 |   ^ ^^^^     ^
+_________________|________________________________________
+                 |
+  op param decl  |  (name:sot)
+                 |  ^^^^^^   ^
+_________________|________________________________________
+                 |
+ op object decl  |  (name:pat)
+                 |  ^^^^^^   ^
+_________________|________________________________________
+                 |
+ op object defn  |  (pat:pat)
+                 |  ^   ^^^^^
+_________________|________________________________________
+                 |
+  op param defn  |  \x,y.pat
+                 |  ^^^^^
+_________________|________________________________________
+                 |
+   actor let     |  let (x : type) = expr.
+                 |      ^        ^
+_________________|________________________________________
+                 |
+  actor fresh    |  make (x,y,z : sot).
+                 |       ^ ^^^^      ^
+_________________|________________________________________
+                 |
+  actor under    |  ^(x,y,z : type).
+                 |   ^ ^^^^       ^
+_________________|________________________________________
+
+  in judgementform postcondition:
+    replace (op [thingy] decl) by schematic variable x means
+      (x : _)       in object position
+      (x : itstype) in param position
+    e.g.
+      {type T}
+      check T t
+      { t -['eq T-'Value] : 'Bool}
diff --git a/test/bothinputoutput.act b/test/bothinputoutput.act
new file mode 100644
index 0000000..e3c81c3
--- /dev/null
+++ b/test/bothinputoutput.act
@@ -0,0 +1,24 @@
+------------------------------------------------------------------------------
+-- Datatypes
+
+syntax
+  { 'Type = ['EnumOrTag  ['Nat]
+                         [['Arr 'Type 'Type]]
+            ]
+  }
+
+syntax
+  { 'Check = ['Tag [ ['Lam ['Bind 'Synth 'Check]]
+                     ['Emb 'Synth]
+             ]]
+  ; 'Synth = ['Tag [ ['Ann 'Check 'Type]
+                     ['App 'Synth 'Check]
+             ]]
+  }
+
+type : $'Type.
+
+judgementform
+  {type T}
+  check T (t : 'Check => T - 'Value)
+  {type T}
diff --git a/test/duplicated-tag.act b/test/duplicated-tag.act
new file mode 100644
index 0000000..fdee5d0
--- /dev/null
+++ b/test/duplicated-tag.act
@@ -0,0 +1 @@
+syntax { 'Type = ['Enum ['A 'A]] }
\ No newline at end of file
diff --git a/test/duplicatedinput.act b/test/duplicatedinput.act
new file mode 100644
index 0000000..e4f50a5
--- /dev/null
+++ b/test/duplicatedinput.act
@@ -0,0 +1,24 @@
+------------------------------------------------------------------------------
+-- Datatypes
+
+syntax
+  { 'Type = ['EnumOrTag  ['Nat]
+                         [['Arr 'Type 'Type]]
+            ]
+  }
+
+syntax
+  { 'Check = ['Tag [ ['Lam ['Bind 'Synth 'Check]]
+                     ['Emb 'Synth]
+             ]]
+  ; 'Synth = ['Tag [ ['Ann 'Check 'Type]
+                     ['App 'Synth 'Check]
+             ]]
+  }
+
+type : $'Type.
+
+judgementform
+  {type T ; type T}
+  check T (t : 'Check => T - 'Value)
+  {}
diff --git a/test/duplicatedoutput.act b/test/duplicatedoutput.act
new file mode 100644
index 0000000..e3e02cf
--- /dev/null
+++ b/test/duplicatedoutput.act
@@ -0,0 +1,24 @@
+------------------------------------------------------------------------------
+-- Datatypes
+
+syntax
+  { 'Type = ['EnumOrTag  ['Nat]
+                         [['Arr 'Type 'Type]]
+            ]
+  }
+
+syntax
+  { 'Check = ['Tag [ ['Lam ['Bind 'Synth 'Check]]
+                     ['Emb 'Synth]
+             ]]
+  ; 'Synth = ['Tag [ ['Ann 'Check 'Type]
+                     ['App 'Synth 'Check]
+             ]]
+  }
+
+type : $'Type.
+
+judgementform
+  {}
+  check T (t : 'Check => T - 'Value)
+  {type T ; type T}
diff --git a/test/golden/bothinputoutput.gold b/test/golden/bothinputoutput.gold
new file mode 100644
index 0000000..48694a1
--- /dev/null
+++ b/test/golden/bothinputoutput.gold
@@ -0,0 +1,11 @@
+ret > ExitFailure 1
+out > Error
+out >
+out >  20 | 
+out >  21 | judgementform
+out >  22 |   {type T}
+out >               ^
+out > bothinputoutput.act:22:8-9
+out > T is both an input and an output
+out > when elaborating the judgement form check
+out >
diff --git a/test/golden/duplicatedinput.gold b/test/golden/duplicatedinput.gold
new file mode 100644
index 0000000..52e0670
--- /dev/null
+++ b/test/golden/duplicatedinput.gold
@@ -0,0 +1,11 @@
+ret > ExitFailure 1
+out > Error
+out >
+out >  20 | 
+out >  21 | judgementform
+out >  22 |   {type T ; type T}
+out >               ^
+out > duplicatedinput.act:22:8-9
+out > T is a duplicated input
+out > when elaborating the judgement form check
+out >
diff --git a/test/golden/duplicatedoutput.gold b/test/golden/duplicatedoutput.gold
new file mode 100644
index 0000000..f33f6fc
--- /dev/null
+++ b/test/golden/duplicatedoutput.gold
@@ -0,0 +1,11 @@
+ret > ExitFailure 1
+out > Error
+out >
+out >  22 |   {}
+out >  23 |   check T (t : 'Check => T - 'Value)
+out >  24 |   {type T ; type T}
+out >               ^
+out > duplicatedoutput.act:24:8-9
+out > T is a duplicated output
+out > when elaborating the judgement form check
+out >
diff --git a/test/golden/judgement-operator.gold b/test/golden/judgement-operator.gold
new file mode 100644
index 0000000..adde22d
--- /dev/null
+++ b/test/golden/judgement-operator.gold
@@ -0,0 +1,11 @@
+ret > ExitFailure 1
+out > Error
+out >
+out >   9 |   }
+out >  10 | 
+out >  11 | exec 'Type?T. PRINTF "%n" T - 'inhabitant.
+out >                                 ^^^^^^^^^^^^^^^
+out > judgement-operator.act:11:26-41
+out > Inferred object description 'Type does not match pattern 'Semantics
+out > when elaborating an exec statement
+out >
diff --git a/test/golden/judgement-optional-pattern.gold b/test/golden/judgement-optional-pattern.gold
new file mode 100644
index 0000000..25cdeff
--- /dev/null
+++ b/test/golden/judgement-optional-pattern.gold
@@ -0,0 +1,5 @@
+ret > ExitSuccess
+out > 'Nat
+out >
+err >
+err >
diff --git a/test/golden/malformedPostOp.gold b/test/golden/malformedPostOp.gold
new file mode 100644
index 0000000..1356f42
--- /dev/null
+++ b/test/golden/malformedPostOp.gold
@@ -0,0 +1,11 @@
+ret > ExitFailure 1
+out > Error
+out >
+out >  11 |   {}
+out >  12 |   type (T : 'Type)
+out >  13 |   {S - 'Value : 'Semantics}
+out >          ^
+out > malformedPostOp.act:13:3-4
+out > Malformed operator Value; expected it to act on the subject T
+out > when elaborating the judgement form type
+out >
diff --git a/test/golden/missinginput.gold b/test/golden/missinginput.gold
new file mode 100644
index 0000000..31f2b91
--- /dev/null
+++ b/test/golden/missinginput.gold
@@ -0,0 +1,11 @@
+ret > ExitFailure 1
+out > Error
+out >
+out >  19 | judgementform
+out >  20 |   {}
+out >  21 |   check T (t : 'Check => T - 'Value)
+out >               ^
+out > missinginput.act:21:8-9
+out > Found T as a subject but neither as an input nor an output
+out > when elaborating the judgement form check
+out >
diff --git a/test/judgement-operator.act b/test/judgement-operator.act
new file mode 100644
index 0000000..152bd45
--- /dev/null
+++ b/test/judgement-operator.act
@@ -0,0 +1,11 @@
+syntax { 'Bool = ['Enum ['T 'F]] }
+syntax { 'Type = ['EnumOrTag ['Nat] [['Prod 'Type 'Type]]] }
+
+judgementform
+  {}
+  type (T : 'Type => 'Semantics)
+  { T - 'inhabitant : T
+  ; T -['isInhabitant (_ : T)] : 'Bool
+  }
+
+exec 'Type?T. PRINTF "%n" T - 'inhabitant.
diff --git a/test/judgement-optional-pattern.act b/test/judgement-optional-pattern.act
new file mode 100644
index 0000000..690b0f3
--- /dev/null
+++ b/test/judgement-optional-pattern.act
@@ -0,0 +1,14 @@
+syntax { 'Type = ['Enum ['Nat 'Bool]] }
+
+sem : $'Wildcard.
+
+judgementform
+  {sem A; sem B}
+  judge A B (t : 'Type => ['Pi A \x.B])
+  {t {-: ['Pi A \x.B]-} -['action (x : A)] : B}
+
+operator
+  { f : ['Pi A \x.B] -['action x] ~> f -['app x]
+  }
+
+exec ['Pi 'Type \_.'Type]?f. (f ~ \ X. X | PRINTF "%n" f -['action 'Nat].)
diff --git a/test/malformedPostOp.act b/test/malformedPostOp.act
new file mode 100644
index 0000000..5c1b2b9
--- /dev/null
+++ b/test/malformedPostOp.act
@@ -0,0 +1,13 @@
+------------------------------------------------------------------------------
+-- Datatypes
+
+syntax
+  { 'Type = ['EnumOrTag  ['Nat]
+                         [['Arr 'Type 'Type]]
+            ]
+  }
+
+judgementform
+  {}
+  type (T : 'Type)
+  {S - 'Value : 'Semantics}
diff --git a/test/missinginput.act b/test/missinginput.act
new file mode 100644
index 0000000..7878265
--- /dev/null
+++ b/test/missinginput.act
@@ -0,0 +1,22 @@
+------------------------------------------------------------------------------
+-- Datatypes
+
+syntax
+  { 'Type = ['EnumOrTag  ['Nat]
+                         [['Arr 'Type 'Type]]
+            ]
+  }
+
+syntax
+  { 'Check = ['Tag [ ['Lam ['Bind 'Synth 'Check]]
+                     ['Emb 'Synth]
+             ]]
+  ; 'Synth = ['Tag [ ['Ann 'Check 'Type]
+                     ['App 'Synth 'Check]
+             ]]
+  }
+
+judgementform
+  {}
+  check T (t : 'Check => T - 'Value)
+  {}
diff --git a/test/operator-elab-fail-3.act b/test/operator-elab-fail-3.act
index fdce8ff..81af4e5 100644
--- a/test/operator-elab-fail-3.act
+++ b/test/operator-elab-fail-3.act
@@ -5,4 +5,4 @@ operator { (b : 'Bool) - ['if (t : 'Wildcard) (e : 'Wildcard)] : 'Wildcard }
 operator
   { 'True  : 'Bool - ['if l r] ~> l
   ; 'False : 'Bool - ['ifte l r] ~> r
-  }
+  }
\ No newline at end of file
diff --git a/test/operator-elab-fail-4.act b/test/operator-elab-fail-4.act
index 8b9554c..8f9d68b 100644
--- a/test/operator-elab-fail-4.act
+++ b/test/operator-elab-fail-4.act
@@ -2,7 +2,6 @@ syntax { 'Bool = ['Enum ['False 'True]] }
 
 operator { (b : 'Boo) - ['if (t : 'Wildcard) (e : 'Wildcard)] : 'Wildcard }
 
-
 operator
   { 'True : 'Bool - ['if l r] ~> l
   ; 'False : 'Bool - ['if l r] ~> r
diff --git a/test/reduce-neutrals-2.act b/test/reduce-neutrals-2.act
index 4ca3495..ba036f7 100644
--- a/test/reduce-neutrals-2.act
+++ b/test/reduce-neutrals-2.act
@@ -5,4 +5,4 @@ operator
 
 operator { x : X - ['fst b1] : _ - ['snd b2] ~> x - ['fst b1 - ['snd b2]] }
 
-exec (['Enum ['True]]?b1 b2. let a : 'Atom = 'at . a - ['fst b1] - ['snd b2] ~ a - ['fst b1 - ['snd b2]])
+exec (['Enum ['True]]?b1 b2. let a : 'Atom = 'at . a - ['fst b1] - ['snd b2] ~ a - ['fst b1 - ['snd b2]])
\ No newline at end of file
diff --git a/test/sot-operator.act b/test/sot-operator.act
new file mode 100644
index 0000000..73a38f3
--- /dev/null
+++ b/test/sot-operator.act
@@ -0,0 +1,10 @@
+syntax { 'Nat = ['EnumOrTag ['Zero] [['Succ 'Nat]]] }
+
+operator
+  { (n : 'Nat) -['elim (P : 'Nat\x.'Semantics)
+                       (base : {x='Zero}P)
+                       (step : 'Nat\y.{x=y}P\ih.{x=['Succ y]}P) ] : {x=n}P
+  ; 'Zero : 'Nat -['elim \x.P base \y ih.step] ~> base
+  ; ['Succ n] : 'Nat -['elim \x.P base \y ih.step]
+      ~> {y = n, ih = n -['elim \x.P base \y ih.step]}step
+  }
diff --git a/test/stlcRules.act b/test/stlcRules.act
new file mode 100644
index 0000000..6e9ef8b
--- /dev/null
+++ b/test/stlcRules.act
@@ -0,0 +1,142 @@
+------------------------------------------------------------------------------
+-- Datatypes
+
+syntax
+  { 'Type = ['EnumOrTag  ['Nat]
+                         [['Arr 'Type 'Type]]
+            ]
+  }
+
+syntax
+  { 'Check = ['Tag [ ['Lam ['Bind 'Synth 'Check]]
+                     ['Emb 'Synth]
+             ]]
+  ; 'Synth = ['Tag [ ['Ann 'Check 'Type]
+                     ['App 'Synth 'Check]
+             ]]
+  }
+
+-- this is in 'Semantics, or so we declare
+syntax -- we're calling in not-'Nat on purpose
+  { 'Natural = ['EnumOrTag ['Zero]
+                           [['Succ 'Natural]]
+               ]
+  }
+
+{-
+-----------------------------------------------------------------------------
+-- Judgement forms
+
+/type : $'Type.
+check : ?'Type. $'Check.
+synth : $'Synth. !'Type.
+
+
+-- | myCtxt maps synthesisable variables to types
+myCtxt |- 'Synth -> 'Type
+-}
+
+------------------------------------------------------------------------------
+-- Judgement forms and their contracts
+
+-- Something that looks like "Z : A => B" says
+-- Z is an A when it's a subject, and a B when it becomes a citizen
+
+judgementform
+  {}
+  type (T : 'Type) -- no '=> B' means the citizen version is the same
+  {T - 'Value : 'Semantics}
+
+judgementform
+  {type T}
+  check T (t : 'Check => T - 'Value)
+  { (t : _) -['Bla (T : _)]: 'Semantics
+  ; (t : _) -['eq (_ : T -'Value)] : 'Bool}
+
+judgementform
+  {}
+  synth (e : 'Synth => S - 'Value) S
+  {type S; e -'Quote : 'Check}
+
+
+-- Open question in the above: will it always be the subject that's fed to an operator?
+-- Note: the "T - 'Value" is in 'Semantics and that T is the citizen, not the subject
+
+-- {} myCtxt |- x -> T {synth x T}
+
+rule
+  {}
+  type 'Nat
+  {'Nat - 'Value ~> 'Natural}
+
+
+rule
+  {type S; type T}
+  ------------------------
+  type ['Arr S T] => ['Arr S T]
+-- Global assumption: 'Semantics comes with Pi builtin
+  {['Arr S T] - 'Value ~> ['Pi (S - 'Value) \_. (T - 'Value)]}
+
+-- Invariant: the subject in a premise is always something with a name
+-- payoff - the name BECOMES the name of the citizen
+
+rule
+  { \ x . synth x S |- check T body }
+  -- x is a hypothetical inhabitant of S - 'Value
+  -- hypothetical judgement with fresh x, assuming `synth x S`
+  -- (note hypothetical judgements have patterns in input and subject
+  --  positions, and expressions in output positions)
+  check ~['Arr S T] ['Lam \x. body] => (\x. body)
+  -- ~['Arr S T] means to not match, but to constrain instead
+  {}
+-- Could equivalently be written without deliberate capture of x:
+--  { \ y . synth y S |- check T {x=y}body }
+       -- note that if we use the above, then we'd expect to capture a y in S - 'Value in body the citizen
+       -- the elaborator-check that body is used fully generally in the premiss subject
+       -- needs to return the variables that are in scope for body the citizen
+
+rule
+  { synth e S
+  ; S = T -- by the magic of STLC, things are first-order, this is just unification
+  }
+  check T ['Emb e] => e
+  {}
+
+-- first arg is a (subject) pattern position
+-- 2nd argument is in output position & we give the citizen T
+--   Note to selves: holy readability issues!
+
+rule
+  { type T
+  ; check T t
+  }
+  synth (['Ann t T] => t) T
+  {}
+
+rule
+  { synth f ~['Arr S T]
+  ; check S s
+  }
+  synth (['App f s] => (f -['app s])) T     -- assuming citizen 'f' is meta-level function
+  -- irrefutable because of no overloading of application (in STLC)
+  {}
+
+------------------------------------------------------------------------------
+
+
+------------------------------------------------------------------------------
+-- Examples
+{-
+exec check@p. p! ['Arr 'Nat ['Arr 'Nat 'Nat]].
+              p! ['Lam \z. ['Lam \_. ['Emb z]]].
+exec check@p. p! ['Arr 'Nat 'Nat].
+              p! ['Lam \z. ['Emb z]].
+
+
+exec check@p.
+   p! ['Arr 'Nat 'Nat].
+   p! ['Lam \z. ['Emb
+         ['App ['Ann ['Lam \w. ['Emb w]] ['Arr 'Nat 'Nat]]
+         ['Emb z]]]].
+   PRINTF "Victory!".
+-}
diff --git a/test/telescopic-protocols.act b/test/telescopic-protocols.act
new file mode 100644
index 0000000..629e09c
--- /dev/null
+++ b/test/telescopic-protocols.act
@@ -0,0 +1,20 @@
+syntax
+  { 'Bool = ['Enum ['True 'False]]
+  ; 'Type = ['EnumOrTag ['Base] [['Arr 'Type 'Type]]]
+  }
+
+operator
+  { (T : 'Type) - 'Meaning : 'Semantics
+  ; 'Base : 'Type -'Meaning ~> 'Bool
+  ; ['Arr A B] : 'Type -'Meaning ~> ['Pi (A -'Meaning) \ _. (B -'Meaning)]
+  }
+
+inhab : ?A : 'Type. ! A -'Meaning.
+inhab@p = p?A. case A
+  { 'Base -> p!'True.
+  ; ['Arr S T] -> inhab@q. q!T. q?t. p!\_.t.
+  }
+
+exec inhab@p. p!['Arr 'Base ['Arr 'Base 'Base]].
+              p?t.
+              PRINTF "My favourite inhabitant is %i" t.
diff --git a/typos.cabal b/typos.cabal
index 4f7ddbd..9f44ebd 100644
--- a/typos.cabal
+++ b/typos.cabal
@@ -65,6 +65,7 @@ library
                        Pattern,
                        Pattern.Coverage,
                        Pretty,
+                       Rules,
                        Scope,
                        Semantics,
                        Syntax,