trackoor / STLC Public

Notifications You must be signed in to change notification settings
Fork 0
Star 5

❄️ Simply typed lambda calculus formalized in Coq, REPL in Haskell.

5 stars 0 forks Branches Tags Activity

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 11 Commits
Main.hs		Main.hs
Parser.hs		Parser.hs
README.md		README.md
STLC.hs		STLC.hs
STLC.v		STLC.v

Repository files navigation

STLC

Try to implement a STLC REPL in Coq & Haskell. Formalized in Coq, Run in Haskell.

TODO

Formally verify some feature of this implementation in Coq
De bruijn Index

About

❄️ Simply typed lambda calculus formalized in Coq, REPL in Haskell.

programming-language stlc simply-typed-lambda-calculus

Report repository

Releases

No releases published

Languages