Lean
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Verified Decision Procedures for Modal Logics.
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Eliminating dependent pattern matching without K
- Characteristics of de Bruijn’s early proof checker Automath
- Herbrand constructivization for automated intuitionistic theorem proving
- RustHorn: CHC-based verification for Rust programs
- Verification of dynamic bisimulation theorems in Coq
- A formalization of Dedekind domains and class groups of global fields
- From the universality of mathematical truth to the interoperability of proof systems
- Flexible proof production in an industrial-strength SMT solver
- Schemes in Lean
- scientific article; zbMATH DE number 7327936 (Why is no real title available?)
- A web-based toolkit for mathematical word processing applications with semantics
- Interpreting mathematical texts in Naproche-SAD
- Maintaining a library of formal mathematics
- On a machine-checked proof for fraction arithmetic over a GCD domain
- ProofWidgets
- A Coq formalization of Lebesgue integration of nonnegative functions
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- Aligning concepts across proof assistant libraries
- scientific article; zbMATH DE number 7649955 (Why is no real title available?)
- Higher groups in homotopy type theory
- Formalizing geometric algebra in Lean
- A language with type-dependent equality
- scientific article; zbMATH DE number 7649968 (Why is no real title available?)
- A certified program for the Karatsuba method to multiply polynomials
- Declarative Proof Translation (Short Paper)
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Semantic representation of general topology in the Wolfram language
- An extensible equality checking algorithm for dependent type theories
- Simple type theory is not too simple: Grothendieck's schemes without dependent types
- The homological arrow polynomial for virtual links
- Coq
- KANT/KASH
- KeY-C
- Nitpick
- TkWinHOL
- Isabelle/HOL
- Isabelle/Isar
- CoqEAL
- Algolib
- Mizar
- Kenzo
- Isabelle/ZF
- Matita
- HOL Light
- Isabelle/PIDE
- QMT
- Lurch
- Polar
- AutPGrp
- Agda
- Epigram
- CalcCheck
- Irdis
- ForTheL
- Gmeta
- LNgen
- Quantomatic
- TLPVS
- Poly/ML
- Coquelicot
- Manip
- Autoref
- Eisbach
- Aglet
- Metamath
- dedukti
- Vellvm
- McBits
- HoTT
- MathScheme
- UniMath
- MedOlDatschgerl
- AUTO2
- Globular
- miz3
- CoqMTU
- CkAnalytic
- Idris
- Pilsner
- XBarnacle
- AmiCo
- Literate CoffeeScript
- Markdown
- MathQuill
- nsoks
- webLurch
- Transfer
- GRAT
- cubicaltt
- jsfs
- AGREE
- Jordan
- kepler98
- MathOverflow
- RedPRL
- HOLCF
- TinyMCE
- HoTTSQL
This page was built for software: Lean
