This repository contains a formal proof of the type soundness of the Simply Typed Lambda Calculus (STLC) using Coq. The proof demonstrates that well-typed terms satisfy progress (a term is either a value or can take a step) and preservation (evaluation preserves types).
-
Notifications
You must be signed in to change notification settings - Fork 0
RINNE-TAN/STLC
About
Formal proof of STLC type soundness (progress and preservation) using Coq.
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published