Topic: "lambda-calculus"
HigherOrderCO/Kind
A modern proof language
Language: Haskell - Size: 34.6 MB - Last synced at: 7 days ago - Pushed at: 10 months ago - Stars: 3,703 - Forks: 147
sdiehl/write-you-a-haskell
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
Language: Haskell - Size: 938 KB - Last synced at: 6 months ago - Pushed at: almost 5 years ago - Stars: 3,379 - Forks: 256
JasonShin/fp-core.rs
A library for functional programming in Rust
Language: Rust - Size: 271 KB - Last synced at: 6 months ago - Pushed at: over 3 years ago - Stars: 1,377 - Forks: 66
niltok/magic-in-ten-mins
十分钟魔法练习
Language: HTML - Size: 31.5 MB - Last synced at: 8 months ago - Pushed at: about 2 years ago - Stars: 800 - Forks: 38
HOL-Theorem-Prover/HOL
Canonical 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.
Language: Standard ML - Size: 129 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 697 - Forks: 161
woodrush/lambda-8cc
x86 C compiler written in untyped lambda calculus
Language: Common Lisp - Size: 1.47 MB - Last synced at: 6 months ago - Pushed at: about 3 years ago - Stars: 657 - Forks: 16
glebec/lambda-talk
A Flock of Functions: Combinators, Lambda Calculus, & Church Encodings in JS
Language: JavaScript - Size: 476 KB - Last synced at: 6 months ago - Pushed at: almost 2 years ago - Stars: 521 - Forks: 42
slovnicki/pLam
An interpreter for learning and exploring pure λ-calculus
Language: Haskell - Size: 1.1 MB - Last synced at: 6 months ago - Pushed at: over 4 years ago - Stars: 460 - Forks: 17
cedille/cedille
Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations
Language: Agda - Size: 19.3 MB - Last synced at: 8 months ago - Pushed at: about 2 years ago - Stars: 374 - Forks: 27
Chymyst/curryhoward
Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
Language: Scala - Size: 428 KB - Last synced at: about 1 month ago - Pushed at: 6 months ago - Stars: 260 - Forks: 18
cognate-lang/cognate
A human readable quasi-concatenative programming language
Language: C - Size: 4.45 MB - Last synced at: 7 months ago - Pushed at: 9 months ago - Stars: 251 - Forks: 12
woodrush/lambdalisp
A Lisp interpreter written in untyped lambda calculus
Language: Common Lisp - Size: 1.11 MB - Last synced at: about 1 month ago - Pushed at: over 2 years ago - Stars: 244 - Forks: 11
lazear/types-and-programming-languages
Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!
Language: Rust - Size: 567 KB - Last synced at: 7 months ago - Pushed at: over 5 years ago - Stars: 206 - Forks: 10
ucsd-progsys/elsa
Elsa is a lambda calculus evaluator
Language: Haskell - Size: 118 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 189 - Forks: 24
lambda-study-group/awesome-functional-studies
A curated list of functional programming resources to study the fp paradigm
Size: 94.7 KB - Last synced at: 11 days ago - Pushed at: over 1 year ago - Stars: 181 - Forks: 17
chibicode/Y-Combinator-for-Non-programmers
🍱 Y Combinator for Non-programmers: A Wild Introduction to Computer Science
Language: TypeScript - Size: 14.9 MB - Last synced at: 3 months ago - Pushed at: over 2 years ago - Stars: 162 - Forks: 7
discus-lang/iron
Coq formalizations of functional languages.
Language: Coq - Size: 800 KB - Last synced at: 7 months ago - Pushed at: over 5 years ago - Stars: 143 - Forks: 8
benji6/combinators-js
:bird: Some combinators
Language: JavaScript - Size: 271 KB - Last synced at: 21 days ago - Pushed at: 11 months ago - Stars: 138 - Forks: 8
polux/lambda-diagrams
Animations of lambda term reduction sequences
Language: Haskell - Size: 10.7 KB - Last synced at: 4 months ago - Pushed at: over 7 years ago - Stars: 138 - Forks: 8
chorasimilarity/chemlambda-gui
Life like molecular computers with artificial chemistry.
Language: HTML - Size: 26.4 MB - Last synced at: over 1 year ago - Pushed at: about 3 years ago - Stars: 134 - Forks: 14
ljedrz/lambda_calculus
A simple, zero-dependency implementation of the untyped lambda calculus in Safe Rust
Language: Rust - Size: 653 KB - Last synced at: 13 days ago - Pushed at: about 2 months ago - Stars: 133 - Forks: 15
benji6/church
:church: Church Encoding in JS
Language: JavaScript - Size: 935 KB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 127 - Forks: 10
marvinborner/bruijn
:abacus: Programming with pure lambda calculus
Language: Haskell - Size: 1.49 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 127 - Forks: 0
Lambda-Mountain-Compiler-Backend/LSTS
Large Scale Type Systems: ML/C Hybrid Programming Language
Size: 1.22 MB - Last synced at: 5 days ago - Pushed at: 3 months ago - Stars: 124 - Forks: 3
abella-prover/abella
An interactive theorem prover based on lambda-tree syntax
Language: OCaml - Size: 4.55 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 98 - Forks: 19
sgillespie/lambda-calculus
An introduction to the Lambda Calculus
Size: 146 KB - Last synced at: 1 day ago - Pushed at: over 3 years ago - Stars: 94 - Forks: 15
gtramontina/lambda
Fun with λ calculus!
Language: JavaScript - Size: 10.7 KB - Last synced at: 4 months ago - Pushed at: over 4 years ago - Stars: 90 - Forks: 8
zehaochen19/vanilla-lang
An implementation of a predicative polymorphic language with bidirectional type inference and algebraic data types
Language: Haskell - Size: 255 KB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 88 - Forks: 3
orsinium-labs/python-lambda-calculus
Lambda Calculus things implemented on Python
Language: Python - Size: 41 KB - Last synced at: 3 months ago - Pushed at: about 6 years ago - Stars: 88 - Forks: 9
sjsyrek/malc
Make a lambda calculus.
Language: Python - Size: 67.4 KB - Last synced at: 7 months ago - Pushed at: about 5 years ago - Stars: 85 - Forks: 11
clark800/lambda-zero
minimalist pure lazy functional programming language (pythonic haskell)
Language: C - Size: 1.78 MB - Last synced at: about 2 months ago - Pushed at: 8 months ago - Stars: 78 - Forks: 5
bor0/gidti
Book: Introduction to Dependent Types with Idris
Size: 10.9 MB - Last synced at: 6 months ago - Pushed at: over 2 years ago - Stars: 78 - Forks: 4
marvinborner/birb
:bird: *cheep cheep shriek caw*
Language: Haskell - Size: 45.9 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 73 - Forks: 4
mroman42/mikrokosmos
(λ) Educational lambda calculus interpreter
Language: Haskell - Size: 3.27 MB - Last synced at: 19 days ago - Pushed at: over 4 years ago - Stars: 73 - Forks: 7
moonad-archive/Formality-JavaScript
An implementation of the Formality language in JavaScript
Language: JavaScript - Size: 6.28 MB - Last synced at: about 1 month ago - Pushed at: about 6 years ago - Stars: 71 - Forks: 4
orsinium-labs/rlci
🦀 λ Overly-documented Rust-powered Lambda Calculus Interpreter.
Language: Rust - Size: 88.9 KB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 64 - Forks: 1
discus-lang/salt
The compilation target that functional programmers always wanted.
Language: Haskell - Size: 1.07 MB - Last synced at: 7 months ago - Pushed at: over 5 years ago - Stars: 62 - Forks: 3
WhatisRT/meta-cedille
Minimalistic dependent type theory with syntactic metaprogramming
Language: Agda - Size: 945 KB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 57 - Forks: 0
cdparks/lambda-machine
A simple UI for evaluating expressions in the untyped lambda calculus
Language: PureScript - Size: 3.37 MB - Last synced at: over 1 year ago - Pushed at: almost 3 years ago - Stars: 55 - Forks: 3
ngzhian/ski
SKI combinators
Language: OCaml - Size: 19.5 KB - Last synced at: 4 months ago - Pushed at: over 8 years ago - Stars: 55 - Forks: 1
steshaw/lennart-lambda
λλλλ Lennart Augustsson's λ-calculus cooked four ways
Language: Haskell - Size: 272 KB - Last synced at: about 1 month ago - Pushed at: over 8 years ago - Stars: 53 - Forks: 11
asperti/BOHM1.1
Bologna Optimal Higher-Order Machine, Version 1.1
Language: C - Size: 291 KB - Last synced at: over 2 years ago - Pushed at: over 8 years ago - Stars: 51 - Forks: 7
jfaure/lfvm-stg
Map lazy functional language constructs to LLVM IR
Language: Haskell - Size: 59.6 KB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 50 - Forks: 0
codedot/lambda
Macro Lambda Calculus
Language: JavaScript - Size: 518 KB - Last synced at: about 2 months ago - Pushed at: over 6 years ago - Stars: 50 - Forks: 3
AndyShiue/pts
implementation of Pure Type Systems (PTS) in Rust.
Language: Rust - Size: 29.3 KB - Last synced at: about 2 years ago - Pushed at: over 8 years ago - Stars: 50 - Forks: 2
wbbradley/ace
A statically-typed strictly-evaluated garbage-collected readable programming language.
Language: C++ - Size: 25.8 MB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 48 - Forks: 2
tarao/LambdaJS
An interpreter of Lambda calculus written in JavaScript and working with JavaScript syntax.
Language: JavaScript - Size: 93.8 KB - Last synced at: 7 months ago - Pushed at: about 7 years ago - Stars: 47 - Forks: 5
andgate/type-theory-compiler
Compiler for type theoretic lambda calculi equipped with system primtives which compiles side-effecting, strict expressions into efficient LLVM IR.
Language: Haskell - Size: 235 KB - Last synced at: over 1 year ago - Pushed at: over 6 years ago - Stars: 42 - Forks: 0
Soonad/Formality-Core
Specification of the Formality proof and programming language
Language: JavaScript - Size: 604 KB - Last synced at: 10 days ago - Pushed at: almost 3 years ago - Stars: 41 - Forks: 11
zhiayang/lambda
lambda calculus interpreter
Language: C++ - Size: 186 KB - Last synced at: 8 months ago - Pushed at: over 4 years ago - Stars: 40 - Forks: 5
etiamz/optiscope
A Lévy-optimal lambda calculus reducer with a backdoor to C
Language: C - Size: 599 KB - Last synced at: 27 days ago - Pushed at: 28 days ago - Stars: 38 - Forks: 0
thma/lambda-ski
Implementing a small functional language with a combinator based graph-reduction machine
Language: Haskell - Size: 747 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 36 - Forks: 3
ltext/ltext
λtext - higher-order file applicator
Language: Haskell - Size: 6.62 MB - Last synced at: 22 days ago - Pushed at: almost 2 years ago - Stars: 36 - Forks: 5
lukeg101/lplzoo
Fine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck
Language: Haskell - Size: 1.96 MB - Last synced at: 6 months ago - Pushed at: over 4 years ago - Stars: 36 - Forks: 2
terremoth/js-church-encoding
Church Encoding Implementation in JavaScript
Language: JavaScript - Size: 16.6 KB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 35 - Forks: 3
mgechev/typed-calc
Interpreter for simply typed lambda calculus implemented in JavaScript λ
Language: JavaScript - Size: 28.3 KB - Last synced at: about 1 month ago - Pushed at: over 8 years ago - Stars: 35 - Forks: 4
marvinborner/interaction-net-resources
:books: Interaction net resources
Size: 57.6 KB - Last synced at: 26 days ago - Pushed at: 27 days ago - Stars: 34 - Forks: 0
Lysxia/system-F
Formalization of the polymorphic lambda calculus and its parametricity theorem
Language: Coq - Size: 12.7 KB - Last synced at: 7 months ago - Pushed at: 8 months ago - Stars: 34 - Forks: 2
gallettilance/magnificATS
Collection of ATS goodness
Language: ATS - Size: 20.2 MB - Last synced at: 2 months ago - Pushed at: almost 6 years ago - Stars: 34 - Forks: 2
cucapra/lambdalab
interactive λ-calculus for learning
Language: TypeScript - Size: 92.8 KB - Last synced at: over 1 year ago - Pushed at: over 6 years ago - Stars: 34 - Forks: 3
techcentaur/Krivine-Machine
Abstract krivine machine implementing call-by-name semantics. In OCaml.
Language: OCaml - Size: 16.6 KB - Last synced at: over 2 years ago - Pushed at: over 7 years ago - Stars: 34 - Forks: 2
tarao/lambda-scala
Type level lambda calculus in Scala
Language: Scala - Size: 97.7 KB - Last synced at: 4 months ago - Pushed at: over 10 years ago - Stars: 33 - Forks: 3
lorepozo/program-induction
A library for program induction and learning representations.
Language: Rust - Size: 800 KB - Last synced at: about 2 months ago - Pushed at: almost 2 years ago - Stars: 31 - Forks: 7
aartaka/lamber
A functional scripting language compiling to pure Lambda Calculus
Language: Common Lisp - Size: 184 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 30 - Forks: 1
tominated/system_f_omega
My Attempt at System Fω with Row-Polymorphism
Language: OCaml - Size: 27.3 KB - Last synced at: 4 months ago - Pushed at: over 4 years ago - Stars: 30 - Forks: 1
lunarcast/lunarflow 📦
Lambda calculus go brrrr
Language: PureScript - Size: 1.64 MB - Last synced at: 4 months ago - Pushed at: over 2 years ago - Stars: 29 - Forks: 0
rawlins/lambda-notebook
Lambda Notebook: Formal Semantics in Jupyter
Language: Python - Size: 5.46 MB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 28 - Forks: 6
xieyuheng/lambda-lisp.js
An implementation of lambda calculus.
Language: TypeScript - Size: 1.28 MB - Last synced at: 17 days ago - Pushed at: 3 months ago - Stars: 27 - Forks: 3
L-TChen/Type-Theory
Lecture note on Lambda Calculus and Types for FLOLAC
Language: TeX - Size: 1.71 MB - Last synced at: 4 months ago - Pushed at: over 1 year ago - Stars: 27 - Forks: 4
woodrush/lambdacraft
Common Lisp DSL for building untyped lambda calculus expressions
Language: Common Lisp - Size: 434 KB - Last synced at: 8 months ago - Pushed at: 11 months ago - Stars: 25 - Forks: 1
iwilare/church-rosser
A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses the infrastructure for λ-terms and substitutions provided by the PLFA book
Language: Agda - Size: 70.3 KB - Last synced at: over 1 year ago - Pushed at: about 3 years ago - Stars: 22 - Forks: 1
gallettilance/ATS-blockchain
⛓️ Blockchain + Smart contracts from scratch
Language: ATS - Size: 15.1 MB - Last synced at: 2 months ago - Pushed at: over 7 years ago - Stars: 21 - Forks: 3
gergoerdi/interaction-nets
Haskell implementation of interaction net-based lambda evaluation
Language: Haskell - Size: 14.6 KB - Last synced at: 3 months ago - Pushed at: over 9 years ago - Stars: 21 - Forks: 0
noti0na1/LambdaCalculus-java
Lambda calculus implemented in Java
Language: Java - Size: 21.5 KB - Last synced at: 7 months ago - Pushed at: almost 9 years ago - Stars: 20 - Forks: 3
OscarSaharoy/lambda-fibonacci
js lambda calculus implementation of the fibonacci sequence
Language: JavaScript - Size: 71.3 KB - Last synced at: 7 months ago - Pushed at: almost 4 years ago - Stars: 19 - Forks: 0
toadharvard/Lambada
Step-by-step Lambda calculus interpreter for AO, CBN, CBV, NOR strategies
Language: OCaml - Size: 13.7 KB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 18 - Forks: 1
noamz/linlam
a library for experimental linear lambda calculus
Language: Haskell - Size: 157 KB - Last synced at: over 2 years ago - Pushed at: over 2 years ago - Stars: 18 - Forks: 0
NicklasBoto/funQ
Functional Quantum Programming
Language: Haskell - Size: 17.3 MB - Last synced at: over 2 years ago - Pushed at: over 4 years ago - Stars: 18 - Forks: 1
lucpod/aws-lambda-workshop
Some incremental examples suitable to host an AWS Lambda Functions workshop
Language: JavaScript - Size: 416 KB - Last synced at: 6 months ago - Pushed at: over 6 years ago - Stars: 18 - Forks: 4
alangpierce/LambdaCalculusPlayground
An Android app that provides a visual interface for creating and evaluating lambda calculus expressions
Language: JavaScript - Size: 1.23 MB - Last synced at: 7 months ago - Pushed at: over 9 years ago - Stars: 18 - Forks: 1
kayceesrk/cs3100_m25
IITM Paradigms of Programming -- Monsoon 2025
Language: Jupyter Notebook - Size: 32.7 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 17 - Forks: 6
ncfavier/glam
Polymorphic guarded λ-calculus
Language: Haskell - Size: 3.63 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 17 - Forks: 0
gurbaaz27/typeless
an interpreter for λ-calculus implemented in ruby
Language: Ruby - Size: 226 KB - Last synced at: 18 days ago - Pushed at: over 1 year ago - Stars: 17 - Forks: 1
iczelia/blc-mb
Binary Lambda Calculus evaluation engine written in Malbolge.
Language: C - Size: 4.11 MB - Last synced at: 3 months ago - Pushed at: over 3 years ago - Stars: 17 - Forks: 2
groupoid/alonzo
🧊 Типізоване -גчислення
Language: OCaml - Size: 201 KB - Last synced at: 24 days ago - Pushed at: 5 months ago - Stars: 16 - Forks: 1
gergoerdi/universe-of-syntax
A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.
Language: Agda - Size: 38.1 KB - Last synced at: 8 months ago - Pushed at: almost 8 years ago - Stars: 16 - Forks: 0
gergoerdi/stlc-agda
STLC-related snippets in Agda
Size: 164 KB - Last synced at: 8 months ago - Pushed at: over 12 years ago - Stars: 16 - Forks: 1
andrew-johnson-4/perplexity
A notational semantic for documenting neural networks through diagrams
Language: HTML - Size: 210 KB - Last synced at: 5 months ago - Pushed at: over 2 years ago - Stars: 15 - Forks: 0
Bubbler-4/StepULC
Efficient and single-steppable ULC evaluation algorithm
Language: Haskell - Size: 10.7 KB - Last synced at: over 2 years ago - Pushed at: over 4 years ago - Stars: 15 - Forks: 1
na0214/linear-lambda-calculus
An implementation of Linear Lambda Calculus.
Language: OCaml - Size: 32.2 KB - Last synced at: 3 months ago - Pushed at: over 5 years ago - Stars: 15 - Forks: 3
aartaka/stdlambda
Standard library for Lambda Calculus, finally making LC a practical programming language.
Size: 56.6 KB - Last synced at: 7 months ago - Pushed at: 10 months ago - Stars: 14 - Forks: 0
rootmos/silly-k
silly-k is an experimental language inspired by K and APL
Language: Scheme - Size: 128 KB - Last synced at: about 1 month ago - Pushed at: about 1 year ago - Stars: 14 - Forks: 0
mbuliga/quinegraphs
Library of js programs and demos for quines in graph-rewriting systems (for now chemlambda and interaction combinators).
Language: JavaScript - Size: 11.1 MB - Last synced at: over 2 years ago - Pushed at: over 2 years ago - Stars: 14 - Forks: 2
woodrush/lambda-calculus-devkit
A collection of lambda calculus interpreters and development tools
Language: Makefile - Size: 421 KB - Last synced at: 8 months ago - Pushed at: about 3 years ago - Stars: 14 - Forks: 1
georgejkaye/lamviz-js
A visualiser for lambda terms as rooted maps.
Language: JavaScript - Size: 14.2 MB - Last synced at: 7 months ago - Pushed at: almost 4 years ago - Stars: 14 - Forks: 0
Genivia/Husky
🐺 Husky is a lazy functional language similar to Haskell, but with a more conventional syntax
Language: Prolog - Size: 122 KB - Last synced at: 7 months ago - Pushed at: about 5 years ago - Stars: 14 - Forks: 1
brendanzab/elm-stlc
Bidirectional type checker for the simply typed lambda calculus
Language: Elm - Size: 15.6 KB - Last synced at: 7 months ago - Pushed at: almost 6 years ago - Stars: 14 - Forks: 1
ElaraLang/elara
Elara is a purely-functional programming language targetting the JVM
Language: Haskell - Size: 6.68 MB - Last synced at: 16 days ago - Pushed at: about 1 month ago - Stars: 13 - Forks: 3
gwr3n/jsdp
A Java Stochastic Dynamic Programming Library
Language: Java - Size: 50.4 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 13 - Forks: 3
thamugadi/call-cc-krivine
A Krivine machine for the call-by-name reduction of lambda calculus (+ call/cc) expressions in Haskell.
Language: Haskell - Size: 65.4 KB - Last synced at: 7 months ago - Pushed at: over 1 year ago - Stars: 13 - Forks: 1
