LSTS
Programming language
A programming language and proof assistant built on top of Rust.
Large Scale Type Systems (programming language)
114 stars
3 watching
3 forks
Language: Rust
last commit: 3 months ago assisted-reasoningastcategory-theorycompilerdependent-typeserror-reportinglambda-calculuslambda-calculus-interpreterlexerlintlstsparserprogramming-languageproof-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 | A proof assistant based on a type theory for synthetic ∞-categories. | 212 |
 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 | 164 |
 lukaszcz/coqhammer | A tool for automating proof search and verification in dependent type theory using machine learning and external provers. | 220 |
 krassowski/jupyterlab-lsp | A tool for integrating language assistance into JupyterLab | 120 |
 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 | 15 |
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 191 |
 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 | 82 |
 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 | 834 |