search

mroman42 / mikrokosmos

(λ) Educational lambda calculus interpreter
https://mroman42.github.io/mikrokosmos
GNU General Public License v3.0
70 stars 7 forks source link

Other type systems #16

Closed mroman42 closed 7 years ago

mroman42 commented 7 years ago

Write an implementation of a simply typed lambda calculus interpreter and look forward to implement other type systems. A symply-typed Mikrokosmos could be used to check proofs on natural deduction (?)

mroman42 commented 7 years ago

Type inference on simply typed lambda calculus has been implemented in 04a9980758808c0324e74add81c3e73ea387bb1a

mroman42 commented 7 years ago

Simple proofs on IPL can be written on this implementation. 05dba8ad6 limits the expressions that can be executed on the simply-typed interpreter