Skip to content

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

trackoor/STLC

Folders and files

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.

Topics

programming-language stlc simply-typed-lambda-calculus

Resources

Stars

Watchers

Forks

Report repository

Releases

No releases published

Languages