83 Open source projects that are alternatives of or similar to types-and-programming-languages

Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)

Fine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck

Lecture note on Lambda Calculus and Types for FLOLAC

A modern proof language

Book: Gentle Introduction to Dependent Types with Idris

Bologna Optimal Higher-Order Machine, Version 1.1

Formalization of the polymorphic lambda calculus and its parametricity theorem

Elsa is a lambda calculus evaluator

🍱 Y Combinator for Non-programmers: A Wild Introduction to Computer Science

Variant types in TypeScript

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.

(λ) Educational lambda calculus interpreter

Reading schedule and our library of pdfs

Macro Lambda Calculus

My undergradate thesis on coinductive types in univalent type theory

lambda calculus interpreter

Coq formalizations of functional languages.

Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.

An implementation of the Formality language in JavaScript

Implementation of the Fibonacci sequence in JS using pure Lambda Calculus

implementation of Pure Type Systems (PTS) in Rust.

SHAPE/S∀F∃: static prover/type-checker for N-D array programming in Scala, a use case of intuitionistic type theory

A statically-typed strictly-evaluated garbage-collected readable programming language.

Some incremental examples suitable to host an AWS Lambda Functions workshop

A research project in path semantics, a re-interpretation of functions for expressing mathematics

Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust

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.

A minimalist pure lazy functional programming language

Type Theory in Type Theory using Cubical Agda

Church Encoding Implementation in JavaScript

An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle

Efficient and single-steppable ULC evaluation algorithm

Homotopy Type Theory proofs in Idris

Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism

The MLPolyR programming language, revived

Minimalistic dependent type theory with syntactic metaprogramming

🐦 Some combinators

An Android app that provides a visual interface for creating and evaluating lambda calculus expressions

⛪️ Church Encoding in JS

A categorical semantics library in Agda.

Fun with λ calculus!

十分钟魔法练习

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

Univalent mathematics in Agda

λtext - higher-order file applicator

An implementation of a predicative polymorphic language with bidirectional type inference and algebraic data types

Formalisation of the linear lambda calculus in Coq

Dependently-typed row-polymorphic programming language, evolved from minitt-rs

A library for functional programming in Rust

Abstract krivine machine implementing call-by-name semantics. In OCaml.

An interpreter for learning and exploring pure λ-calculus

An inference engine for extensional untyped λ-calculus

Cicada Language

A Flock of Functions: Combinators, Lambda Calculus, & Church Encodings in JS

Lambda Notebook: Formal Semantics in Jupyter

🔮 Estudos obscuros de programação funcional

⛓️ Blockchain + Smart contracts from scratch

Lambda calculus go brrrr

The compilation target that functional programmers always wanted.

An introduction to the Lambda Calculus