CurryhowardAutomatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
ElsaElsa is a lambda calculus evaluator
KindA modern proof language
IronCoq formalizations of functional languages.
Church⛪️ Church Encoding in JS
Lambda calculusA simple, zero-dependency implementation of the untyped lambda calculus in Safe Rust
Ptsimplementation of Pure Type Systems (PTS) in Rust.
Ltextλtext - higher-order file applicator
ZionA statically-typed strictly-evaluated garbage-collected readable programming language.
Dblib LinearFormalisation of the linear lambda calculus in Coq
Fp Core.rsA library for functional programming in Rust
HolCanonical sources for HOL4 theorem-proving system. Branch `develop` is where “mainline development” occurs; when `develop` passes our regression tests, `master` is merged forward to catch up.
PlamAn interpreter for learning and exploring pure λ-calculus
Lambda TalkA Flock of Functions: Combinators, Lambda Calculus, & Church Encodings in JS
Lambda🔮 Estudos obscuros de programação funcional
CedilleCedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations
Write You A HaskellBuilding a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
lplzooFine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck
Type-TheoryLecture note on Lambda Calculus and Types for FLOLAC
lambda-fibonacciImplementation of the Fibonacci sequence in JS using pure Lambda Calculus
Krivine-MachineAbstract krivine machine implementing call-by-name semantics. In OCaml.
saltThe compilation target that functional programmers always wanted.
lambdalambda calculus interpreter
LambdaCalculusPlaygroundAn Android app that provides a visual interface for creating and evaluating lambda calculus expressions
vanilla-langAn implementation of a predicative polymorphic language with bidirectional type inference and algebraic data types
system-FFormalization of the polymorphic lambda calculus and its parametricity theorem
meta-cedilleMinimalistic dependent type theory with syntactic metaprogramming
universe-of-syntaxA universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.
pomagmaAn inference engine for extensional untyped λ-calculus
abellaAn interactive theorem prover based on lambda-tree syntax
gidtiBook: Gentle Introduction to Dependent Types with Idris
lambda-zeroA minimalist pure lazy functional programming language
BOHM1.1Bologna Optimal Higher-Order Machine, Version 1.1
StepULCEfficient and single-steppable ULC evaluation algorithm