An interactive theorem prover based on lambda-tree syntax

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

msfl-hl is a lambda-calculus term interpet written in OCaml

🧊 Типізоване ‏-ג‏‎числення

A type theory for unbiased cartesian closed categories.

A compiler of the Lambda-Calculus to 16-bit x86 assembly code

The λ-calculus

Implementation for the lambda lambda-bar calculus (LLBC)

Interpreter for Lamba-expressions

Intensional PCF interpreter

Lenguaje lambda cálculo implementado en OCaml

Step-by-step Lambda calculus interpreter for AO, CBN, CBV, NOR strategies

Interpreter for a functional, expression-based programming language

Lambda Calculus for fun using OCaml

A typed lambda calculus with a set-theoretic type system, that serves as the theoretical basis for other languages with set-theoretic type systems

The OCaml-lite interpreter is a streamlined tool for parsing and executing OCaml-lite programs, offering insights into programming language interpretation with a focus on simplicity and educational value.

Lambda Calculus Interpreter with Definitions

[WIP] A series of tutorials for lambda calculus

An implementation of dependently typed lambda calculus

Lambda Calculus implementations in OCaml.