Coq formalizations of functional languages.

Formalization of the polymorphic lambda calculus and its parametricity theorem

Formalising Turing Machines In Coq (bachelor's thesis)

Formalisation of the linear lambda calculus in Coq

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

Certified LambdaJS semantics and interpreter.

Research to analyze theoretical principles of the Coq Proof Management System

Lambda-Calculi implementations & proofs in Coq

Untyped Lambda Calculus as Initial Object in Cat of Exponential Monads

Formal proofs of some facts about untyped lambda calculus in Coq

Code and examples based on the tutorial 'A Tutorial on [Co-]Inductive Types in Coq' by Eduardo Giménez and Pierre Castéran

A Formalization of Typed and Untyped λ-Calculi in SSReflect-Coq and Agda2

A deBruijn implementation of the untyped lambda calculus implementation focused on equivalence proofs, a self-interpreter, and a verified compiler to SK

Coq formalization of lambda calculus theories with explicit names. (SETTA'23)

Strong normalization and parametricity for System Fω in Coq

A study of a simplified Call-By-Push-Value lambda-calculus in Coq.

Specification, formalization and verification of the XC function from ex lambda calculus in Coq.

A proof of factorization using Takahashi's method

"Languages, Compilers, and Interpreters" Course Material