LSTS
Type Assistant
A programming language and proof assistant built around type theory and lambda calculus.
Large Scale Type Systems (programming language)
114 stars
3 watching
3 forks
Language: Rust
last commit: 7 days ago assisted-reasoningastcategory-theorycompilerdependent-typeserror-reportinglambda-calculuslambda-calculus-interpreterlanguagelexerlintlstsparserproof-assistantrefinement-typesrusttheorem-provertype-checking
Related projects:
| Repository | Description | Stars |
|---|---|---|
 the-little-prover/j-bob | A proof assistant with a formal system for verifying mathematical theorems and proofs | 420 |
 rzk-lang/rzk | An experimental proof assistant built on top of a type theory for synthetic ∞-categories. | 205 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 liamoc/holbert | An interactive proof assistant designed to help with educational mathematics | 161 |
 lukaszcz/coqhammer | A tool for automating proof search and verification in dependent type theory using machine learning and external provers. | 218 |
 krassowski/jupyterlab-lsp | A tool for integrating language assistance into JupyterLab | 118 |
 lambdabot/lambdabot | An IRC bot and apprentice coder tool built in Haskell for interacting with programming concepts and providing learning support. | 164 |
 ilya-klyuchnikov/lambdapi | Reorganization of source code for dependently typed lambda calculus paper to improve readability and understandability | 112 |
 ecrancemerce/trakt | Automates goal preprocessing in proof automation tactics using a custom-built tool | 14 |
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 188 |
 thma/lambda-ski | Implementing a graph-reduction machine for a small functional language based on λ-calculus and combinatory logic | 28 |
 andreasabel/miniagda | A research prototype of a dependently typed language with sized types and variances | 104 |
 uds-psl/mpctt | A research project on using the Coq proof assistant to develop and prove mathematical models of computation in computational type theory | 80 |
 ahgamut/janet | A dynamic language with user scripting capabilities to extend C/C++ programs and automate system tasks. | 5 |
 informalsystems/quint | A specification language with type checking and tooling based on temporal logic of actions | 827 |