Coq formalizations of functional languages.
-
Updated
Jul 2, 2020 - Coq
Coq formalizations of functional languages.
Formalising Turing Machines In Coq (bachelor's thesis)
Formalization of the polymorphic lambda calculus and its parametricity theorem
Lambda Calculi Formalizations in Coq using nested datatypes for a type-safe term representation
Simply-typed lambda calculus and extensions: termination, extrinsic/intrinsic representations, nominal binding techniques
A deBruijn implementation of the untyped lambda calculus implementation focused on equivalence proofs, a self-interpreter, and a verified compiler to SK
"Languages, Compilers, and Interpreters" Course Material
Certified LambdaJS semantics and interpreter.
Lambda-Calculi implementations & proofs in Coq
Research to analyze theoretical principles of the Coq Proof Management System
Code and examples based on the tutorial 'A Tutorial on [Co-]Inductive Types in Coq' by Eduardo Giménez and Pierre Castéran
Formal proofs of some facts about untyped lambda calculus in Coq
Typechecker for Simply-Typed Lambda Calculus (STLC)
Code and examples based on the book 'Certified Programming with Dependent Types' (version: June 30, 2016) by Adam Chlipala.
Untyped Lambda Calculus as Initial Object in Cat of Exponential Monads
Coq Formalisation of "A Fine-Grained Evaluation Strategy for Delimited-Control Operators shift0/dollar"
A Formalization of Typed and Untyped λ-Calculi in SSReflect-Coq and Agda2
Formalisation of the linear lambda calculus in Coq
Coq formalization of lambda calculus theories with explicit names. (SETTA'23)
Add a description, image, and links to the lambda-calculus topic page so that developers can more easily learn about it.
To associate your repository with the lambda-calculus topic, visit your repo's landing page and select "manage topics."