gteege / gentle-isabelle
A gentle introduction to Isabelle and Isabelle/HOL
☆11Updated this week
Alternatives and similar repositories for gentle-isabelle:
Users that are interested in gentle-isabelle are comparing it to the libraries listed below
- A bottom-up approach to a verified implementation of MLTT☆17Updated last month
- A toy example of a verified compiler.☆28Updated this week
- Experiments with SAT solvers with proofs in Lean 4☆56Updated 9 months ago
- LeanSSR: an SSReflect-Like Tactic Language for Lean☆35Updated this week
- A Testing Framework for Lean☆51Updated 2 weeks ago
- WIP collections library for Lean 4☆32Updated 3 weeks ago
- A work-in-progress core language for Agda, in Agda☆48Updated last week
- High level commands to declare a hierarchy based on packed classes☆97Updated last month
- Mechanizations of Type Theories☆28Updated last month
- A repository for material from the reading group on NbE☆17Updated last year
- A Seamless, Interactive Tactic Learner and Prover for Coq☆63Updated last week
- Experiments with some ways of automating reasoning in lean 4☆15Updated 11 months ago
- A Lean4 Formalization of Polynomial Functors☆19Updated last week
- Lean 4 kernel / 'external checker' written in Lean 4☆97Updated last month
- Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]☆56Updated 6 months ago
- A style guide for Coq☆18Updated 3 years ago
- Coq Enhancement Proposals☆56Updated 2 months ago
- Materials for the course "theorem prover lab: applications in programming languages" at KIT, SS2022 edition☆19Updated 2 years ago
- Logical Relation for MLTT in Coq☆24Updated this week
- A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming lan…☆17Updated last year
- Bindings to libclingo for the lean4 prover and programming language!☆11Updated 4 months ago
- A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.☆75Updated 3 weeks ago
- Probabilistic separation logics for verifying higher-order probabilistic programs.☆21Updated this week
- A WIP definitional (co)datatype package for Lean4☆35Updated 3 months ago
- LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.☆60Updated 8 months ago
- Lean 4 port of Iris, a higher-order concurrent separation logic framework☆90Updated last week
- Lean 4 formalization of Rubik's cubes☆29Updated last month
- maze game encoded in Lean 4 syntax☆53Updated 3 months ago
- Lean type-checker written in Scala.☆35Updated 3 years ago
- Coq plugin embedding elpi☆160Updated last week