sequent1
a prototype functional language
which uses sequent calculus as its dependent type system
XIE Yuheng created
code
the implementation written in scheme
example code in sequent1
source code on github
reading
function compose, type cut, and the algebra of logic
this reading is also used to form a paper for scheme workshop 2016
and a demo for the talk at the workshop