We are hiring ! See our job offers.
swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
Raw File
Tip revision: f94b06de7edcb61d3c49f19417e53dc7dc21d552 authored by Anish Tondwalkar on 22 June 2021, 08:13:54 UTC
updated README
Tip revision: f94b06d
linearDSL.fst
module LinearDSL

open FStar.GSet

noeq
type lin (env:set int) : Type =
  | Lin : lin env

assume val var (x:int) : lin (singleton x)
assume val lam (#env:set int) (n:int{~(mem n env)}) (e:lin (union env (singleton n))) : lin env
assume val app (#env1:set int) (#env2:(set int){equal (intersect env1 env2) empty}) (e1:lin env1) (e2:lin env2) : lin (union env1 env2)

val program1 : lin empty
let program1 =
  assume (equal (singleton 1) (union empty (singleton 1)));
  lam 1 (var 1)

val program2 : lin empty
let program2 =
  assume (equal (singleton 1) (union empty (singleton 1)));
  lam 1 (lam 2 (app (var 1) (var 2)))
back to top