remina

this project formalises a dependently typed lambda calculus as an inductive type w.in lean 4. by encoding the syntax via de bruijn indices, the implementation defines the statics and dynamics of a system similar to lambda pi. the core objective is the mechanisation of fundamental metatheory, specifically the proofs of progress and preservation

surface syntax

types

Unit
A * B
A + B
A -[pure]-> B
A -[io]-> B
forall A. T

terms

unit
tick
fun (x : T) -[eff]-> t
tfun A => t
t [T]
(t, u)
fst t
snd t
inl [B] t
inr [A] t
case t of inl x => l | inr y => r