GitHub topics: lambda-calculus

Repositories

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: about 11 hours ago - Pushed at: about 13 hours ago - Stars: 697 - Forks: 161

CoCoSol007/lambca

A tiny Lambda Calculus DSL

Language: Rust - Size: 83 KB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 0 - Forks: 0

MagentaManifold/little-lamb

Mingyuan has a little lamb(da calculus interpreter).

Language: Rust - Size: 115 KB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 1 - Forks: 0

lambada-llc/tree-calculus

Language: TypeScript - Size: 152 KB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 8 - Forks: 1

kayceesrk/cs3100_m25

IITM Paradigms of Programming -- Monsoon 2025

Language: Jupyter Notebook - Size: 32.7 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 17 - Forks: 6

Amitgo1/hapax

🤖 Streamline AI operations with Hapax, the infrastructure layer that ensures continuous service and automatic failover for seamless provider management.

Language: Go - Size: 12.3 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 0 - Forks: 0

ikram001xs/catch-up

📰 Fetch and read the latest news articles from various sources, with support for English and Spanish, using a simple and intuitive interface.

Language: Vue - Size: 1.31 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 1 - Forks: 0

XOTII/catch-up

📰 Catch up on the latest news articles from various sources with this web app featuring a sleek design and easy navigation.

Language: Vue - Size: 1.31 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 0 - Forks: 0

SamirZaiton/kind

🌐 Provision a Kubernetes cluster on Kind with NGINX, TLS, and essential tools for smooth development and staging environments.

Language: Shell - Size: 1.33 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 0 - Forks: 0

Meowcolm024/stlc-agda

stlc in agda

Language: Agda - Size: 2.61 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 0 - Forks: 0

Danelnov/Lambda-Calculus-Formalization

This formalization uses the De Bruijn indices, the objective is to formalize the Church-Rosser theorem

Language: Lean - Size: 50.8 KB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 1 - Forks: 0

binghe/HOL Fork of HOL-Theorem-Prover/HOL

Forked sources of HOL4 (no cv_compute, etc.)

Language: Standard ML - Size: 137 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 7 - Forks: 2

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

HigherOrderCO/Kind

A modern proof language

Language: Haskell - Size: 34.6 MB - Last synced at: 6 days ago - Pushed at: 10 months ago - Stars: 3,703 - Forks: 147

Jemtaly/ProjectLambda

A calculator / programming language based on lambda calculus. 基于 Lambda 演算的简易编程语言。

Language: C++ - Size: 298 KB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 5 - Forks: 0

vitorsouzaalmeida/lc-interpreter

Introduction to the Untyped Lambda Calculus by covering the basics and then writing an Interpreter

Language: OCaml - Size: 6.84 KB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 1 - Forks: 0

pkitazos/lambda-calc

exploration of the λ-calculus

Language: Rust - Size: 47.9 KB - Last synced at: 15 days ago - Pushed at: 15 days ago - Stars: 0 - Forks: 0

thetruezau/LambdaM

The multiary lambda calculus is an extension of the ordinary lambda calculus where an applicative term has a list of terms as arguments.

Language: Rocq Prover - Size: 191 KB - Last synced at: 18 days ago - Pushed at: 18 days ago - Stars: 0 - Forks: 0

ljedrz/lambda_calculus

A simple, zero-dependency implementation of the untyped lambda calculus in Safe Rust

Language: Rust - Size: 653 KB - Last synced at: 12 days ago - Pushed at: about 2 months ago - Stars: 133 - Forks: 15

fritzo/pomagma 📦

Inference engine for extensional untyped λ-calculus

Language: C++ - Size: 7.72 MB - Last synced at: 22 days ago - Pushed at: 23 days ago - Stars: 3 - Forks: 0

dhodgson615/Lambda-Calculus-Interpreter

A pure Lambda Calculus interpreter written in Python 3

Language: Python - Size: 385 KB - Last synced at: 23 days ago - Pushed at: 24 days ago - Stars: 1 - Forks: 0

kbaird/church-numerals

An Elixir module for Church Encoding of numerals

Language: Elixir - Size: 70.3 KB - Last synced at: 24 days ago - Pushed at: 26 days ago - Stars: 2 - Forks: 0

marvinborner/interaction-net-resources

:books: Interaction net resources

Size: 57.6 KB - Last synced at: 25 days ago - Pushed at: 26 days ago - Stars: 34 - Forks: 0

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: 27 days ago - Stars: 38 - Forks: 0

lbagnascom/type-inference

Language: Elm - Size: 185 KB - Last synced at: 23 days ago - Pushed at: 28 days ago - Stars: 0 - Forks: 1

dxrcy/lambda

Parse, reduce, and unify lambda calculus statements

Language: Zig - Size: 384 KB - Last synced at: 29 days ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

keilambda/ttfpi-agda

Formalization of the book "Type Theory and Formal Proof: An Introduction" in Agda

Language: Agda - Size: 67.4 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 4 - Forks: 0

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

xieyuheng/explicit-lisp.js

An implementation of lambda calculus by explicit substitution.

Language: TypeScript - Size: 156 KB - Last synced at: 15 days ago - Pushed at: 3 months ago - Stars: 2 - Forks: 0

xieyuheng/lambda-lisp.js

An implementation of lambda calculus.

Language: TypeScript - Size: 1.28 MB - Last synced at: 16 days ago - Pushed at: 3 months ago - Stars: 27 - Forks: 3

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

ElaraLang/elara

Elara is a purely-functional programming language targetting the JVM

Language: Haskell - Size: 6.68 MB - Last synced at: 15 days ago - Pushed at: about 1 month ago - Stars: 13 - Forks: 3

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

Bohun9/shambda

Transpiler from Lambda Calculus to Bash

Language: TypeScript - Size: 11.7 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

benji6/combinators-js

:bird: Some combinators

Language: JavaScript - Size: 271 KB - Last synced at: 20 days ago - Pushed at: 11 months ago - Stars: 138 - Forks: 8

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

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

sgillespie/lambda-calculus

An introduction to the Lambda Calculus

Size: 146 KB - Last synced at: about 20 hours ago - Pushed at: over 3 years ago - Stars: 94 - Forks: 15

Lemniscate-world/Robust-Lambda

Building a functional untyped lambda calculus interpreter with a visual reduction tracer.

Language: JavaScript - Size: 5.86 KB - Last synced at: 29 days ago - Pushed at: 10 months ago - Stars: 1 - Forks: 0

ygorsimoes/learning-clojure

My journey in the quest to learn Clojure. 🔢

Language: Clojure - Size: 91.8 KB - Last synced at: about 1 month ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0

rawlins/lambda-notebook

Lambda Notebook: Formal Semantics in Jupyter

Language: Python - Size: 5.46 MB - Last synced at: 7 days ago - Pushed at: 8 days ago - Stars: 28 - Forks: 6

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

moix-dev/moix-language

Lenguaje basado en teoría de categorías y cálculo lambda.

Language: Makefile - Size: 17.6 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

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

taimoorzaeem/pl-stuff

PL Theory, Learning & Write-ups

Language: Racket - Size: 151 KB - Last synced at: 28 days ago - Pushed at: 2 months ago - Stars: 1 - Forks: 0

414owen/lambda-repl

JS / jison port of my lambda-calculus reducer

Language: JavaScript - Size: 43.9 KB - Last synced at: about 1 month ago - Pushed at: over 5 years ago - Stars: 3 - Forks: 0

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

severen/sly

A cunning interpreter for the pure untyped λ-calculus.

Language: Haskell - Size: 86.9 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 5 - 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

bmqn/whisp

Stack-based functional programming language.

Language: C++ - Size: 2 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 1 - Forks: 0

ljedrz/blc

Binary lambda calculus

Language: Rust - Size: 63.5 KB - Last synced at: about 2 months ago - Pushed at: almost 8 years ago - Stars: 10 - Forks: 1

bluelhf/lambda-calculus

Lambda calculus modelling, parsing, and reduction in Java

Language: Java - Size: 17.6 KB - Last synced at: 28 days ago - Pushed at: 2 months ago - Stars: 0 - 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

thma/thma.github.io

Lambda is not a four letter word. My blog on all things haskell and FP.

Language: HTML - Size: 7.63 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 4 - Forks: 2

dhodgson615/Lambda-Calculus-Interpreter-C

The C port of the Python version of this repo

Language: C - Size: 257 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0

gwr3n/jsdp

A Java Stochastic Dynamic Programming Library

Language: Java - Size: 50.4 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 13 - Forks: 3

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: 10 days ago - Pushed at: over 1 year ago - Stars: 181 - Forks: 17

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

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

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

yiyunliu/system-f-omega

Strong normalization and parametricity for System Fω in Coq

Language: Coq - Size: 235 KB - Last synced at: 17 days ago - Pushed at: about 1 year ago - Stars: 5 - Forks: 1

marvinborner/strong-reduction-tests

A test suite for strong beta-reduction of the pure, untyped lambda calculus with ~3500 tests

Language: Python - Size: 9.86 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 4 - Forks: 0

qbixxx/LambdaCalculusEngine

Lambda interpreter built in Scala. Supports AST View, CbN, CbV and Free Variables calculations. Fully functional-oriented implementation.

Language: Scala - Size: 169 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 4 - Forks: 1

LebrancWorkshop/Lebranc-Learn-Functional-Programming

I'm learning a Functional Programming by learning its pure math concepts and apply it on functional language like Haskell, Clojure, Elixir, etc.

Language: JavaScript - Size: 207 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 2 - Forks: 3

luca-schlecker/typst-lambdabus

Easily parse, normalize and display simple λ-Calculus expressions.

Language: Typst - Size: 939 KB - Last synced at: 19 days ago - Pushed at: about 1 year ago - Stars: 8 - Forks: 0

kevinlopaq/cmtt

Typechecker for CMTT

Language: Haskell - Size: 109 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

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

kaygun/LambdaOnMagma

A lambda-calculus interpreter implemented on algebraic abstractions such as magmas and catemorphisms.

Language: Scala - Size: 8.79 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

Shade-raid/lambda

Game about lambda calculus

Language: HTML - Size: 37.1 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

StardustDL/lamcal

An online calculator for lambda calculus (λx. y).

Language: Vue - Size: 657 KB - Last synced at: 3 months ago - Pushed at: over 2 years ago - Stars: 9 - Forks: 2

konstantinosKokos/aethel

A packaging of tools for expressing dependency graphs as typed derivations of a multimodal categorial grammar.

Language: Python - Size: 32.8 MB - Last synced at: about 1 month ago - Pushed at: almost 2 years ago - Stars: 4 - Forks: 3

Educorreia932/Recording

🎥 REPL for a polymorphic record-calculus

Language: Haskell - Size: 181 KB - Last synced at: 23 days ago - Pushed at: 7 months ago - Stars: 2 - Forks: 0

WilliamRagstad/lambda_calc

A simple implementation of the untyped lambda calculus

Language: Rust - Size: 77.1 KB - Last synced at: 20 days ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0

wizard7377/SHIFT

Lamed calculus

Language: Haskell - Size: 2.49 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0

yutao-li/programming-languages-coursera

solutions to some extra challenging problems in course "programming languages"

Language: Racket - Size: 25.4 KB - Last synced at: 29 days ago - Pushed at: almost 7 years ago - Stars: 1 - Forks: 0

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

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

ryanashita/LambdaCalculusSolverFSharp

A lambda calculus solver written in F# and .NET, with tests using MSTest framework. Solver (or 'evaluator') consists of a AST, parser (using custom combinator library), and recursive evaluator

Language: F# - Size: 4.18 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0

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

Rudxain/fastlisp

This is not mine. It's an orphan fork

Language: Python - Size: 55.7 KB - Last synced at: 3 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 1

Seeker04/stlc-agda-elab

Agda formalisation of an elaborator for a simply typed language

Language: Agda - Size: 4.98 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

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

EvanZhouDev/twilight

Twilight is a modern lambda calculus runtime and REPL.

Language: TypeScript - Size: 61.2 MB - Last synced at: about 1 month ago - Pushed at: 5 months ago - Stars: 3 - Forks: 0

sacerdot/Crumbling-Abstract-Machines

This repository contains the formalization of part of the theory behind the Crumbling Abstract Machines, that has been introduced and partially developed in Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, and Claudio Sacerdoti Coen. 2019. Crumbling Abstract Machines. In Proceedings of ACM Conference (Conference’17). ACM, New York, NY,USA,39 pages.

Language: Mathematica - Size: 854 KB - Last synced at: 2 months ago - Pushed at: almost 4 years ago - Stars: 2 - Forks: 1