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.
-
Updated
Dec 10, 2017 - Agda
#
simply-typed-lambda-calculus
Here are 12 public repositories matching this topic...
Bidirectional type checker for the simply typed lambda calculus
-
Updated
Feb 4, 2020 - Elm
❄️ Simply typed lambda calculus formalized in Coq, REPL in Haskell.
-
Updated
Feb 1, 2021 - Haskell
SLConf 2024: 타입으로 안전하게 프로그래밍하기
rust algebraic-data-types beamer polymorphism type-system system-f parametric-polymorphism simply-typed-lambda-calculus generalized-algebraic-data-type ad-hoc-polymorphism subtype-polymorphism universal-type
-
Updated
Jan 14, 2024 - TeX
Simply typed and advanced structures in lambda calculus
-
Updated
May 22, 2020 - Coq
Lean4 mechanization of the simply typed lambda calculus and its metatheory including strong normalization
-
Updated
Jun 24, 2026 - Lean
A repository dedicated to the derivation and implementation of type systems. Current system: Extended System F
typechecker pattern-matching type-system system-f parametric-polymorphism universal-quantifiers simply-typed-lambda-calculus
-
Updated
Aug 5, 2017 - Haskell
Interactive lambda calculus playground - parser, type checker, evaluator, proof-tree visualization, and Curry–Howard correspondence, plus a VS Code extension.
react typescript lambda-calculus antlr4 vscode-extension type-checker lambda-calculus-evaluator simply-typed-lambda-calculus curry-howard-isomorphism lambda-calculus-interpreter
-
Updated
Oct 11, 2026 - TypeScript
Collection of TypeScript type challenges with online judge
-
Updated
Jan 5, 2026 - TypeScript
Exercises and project for Programming Language Seminar course at ITU
-
Updated
Jun 3, 2018 - Coq
Introduced subtyping into Simply Typed Lambda Calculus (STLC), allowing for more flexible type assignments following Liskov’s Substitution Principle. We implemented an algorithmically driven type system supporting subtyping, and then expanded it with joins and meets, based on TaPL by Pierce.
-
Updated
May 13, 2025 - OCaml
Add this topic to your repo
To associate your repository with the simply-typed-lambda-calculus topic, visit your repo's landing page and select "manage topics."