jfeser / L2
λ² is a tool for synthesizing functional programs from input-output examples.
☆68Updated 2 years ago
Alternatives and similar repositories for L2:
Users that are interested in L2 are comparing it to the libraries listed below
- EGraphs in OCaml☆64Updated last year
- Coq Protocol Playground with Se(xp)rialization of Internal Structures.☆129Updated 5 months ago
- Offline partial evaluation system for Prolog written using the cogen approach☆19Updated 8 years ago
- SML code for Handbook of Practical Logic and Automated Reasoning - For Isabelle too☆36Updated 8 years ago
- ☆40Updated 6 years ago
- A heuristic procedure for proving inequalities☆33Updated 6 years ago
- [research] A modular SMT solver in OCaml, based on mcSAT☆39Updated last year
- A formalisation of the Calculus of Constructions☆68Updated 8 months ago
- A (formalised) general definition of type theories☆57Updated 3 years ago
- Kleene algebra modulo theories☆27Updated 2 years ago
- A mechanisation of Wasm in Isabelle.☆26Updated this week
- An experimental type checker for a modal dependent type theory.☆110Updated 4 years ago
- Interpreter for the reversible functional language rFun☆36Updated 7 years ago
- Graph Theory [maintainers=@chdoc,@damien-pous]☆35Updated 2 months ago
- A Lustre compiler in Coq☆68Updated 2 weeks ago
- Model finder for higher-order logic☆44Updated last year
- An interactive theorem prover based on lambda-tree syntax☆94Updated 2 months ago
- ☆14Updated 6 years ago
- General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]☆47Updated 5 months ago
- An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logt…☆141Updated 6 months ago
- αProlog☆17Updated last year
- A best-first-search theorem prover implemented in Isabelle☆34Updated 2 years ago
- Coq formalizations and proofs of (data) structures and algorithms.☆46Updated 6 years ago
- Documentation on goals of the Rocq-community organization, the shared contributing guide and code of conduct.☆68Updated 2 weeks ago
- An automated deductive program verifier.☆42Updated 2 years ago
- Implementation of Nuprl's type theory in Coq☆45Updated 4 months ago
- LVC verified compiler☆57Updated 6 years ago
- Synthesis of Heap-Manipulating Programs from Separation Logic☆125Updated 2 years ago
- Mostly Automated Synthesis of Correct-by-Construction Programs☆151Updated 3 weeks ago
- Real number computation software☆123Updated 2 years ago