Pages that link to "Item:Q3454108"
From MaRDI portal
The following pages link to The Lean Theorem Prover (System Description) (Q3454108):
Displaying 50 items.
- Lean (Q27041) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Bellerophon: tactical theorem proving for hybrid systems (Q1687737) (← links)
- Homotopy type theory in Lean (Q1687770) (← links)
- Meaning explanations at higher dimension (Q1688954) (← links)
- Verification of dynamic bisimulation theorems in Coq (Q2035655) (← links)
- The Isabelle/Naproche natural language proof assistant (Q2055899) (← links)
- The Lean 4 theorem prover and programming language (Q2055901) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean} (Q2097420) (← links)
- A formalization of Dedekind domains and class groups of global fields (Q2102929) (← links)
- Formalizing geometric algebra in Lean (Q2128117) (← links)
- A language with type-dependent equality (Q2128827) (← links)
- A certified program for the Karatsuba method to multiply polynomials (Q2132545) (← links)
- Voting theory in the Lean theorem prover (Q2148823) (← links)
- Program logic for higher-order probabilistic programs in Isabelle/HOL (Q2163157) (← links)
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support (Q2211865) (← links)
- On a machine-checked proof for fraction arithmetic over a GCD domain (Q2217198) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Semantic representation of general topology in the Wolfram language (Q2364674) (← links)
- A web-based toolkit for mathematical word processing applications with semantics (Q2364686) (← links)
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge (Q2663667) (← links)
- A Coq formalization of Lebesgue integration of nonnegative functions (Q2673304) (← links)
- A bi-directional extensible interface between Lean and Mathematica (Q2673306) (← links)
- Verification of the ROS NavFn planner using executable specification languages (Q2693303) (← links)
- On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions (Q2798773) (← links)
- Congruence Closure in Intensional Type Theory (Q2817913) (← links)
- Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover (Q2819195) (← links)
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures (Q2829996) (← links)
- Friends with Benefits (Q2988636) (← links)
- (Q3121020) (← links)
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types (Q5016211) (← links)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
- An extensible equality checking algorithm for dependent type theories (Q5028472) (← links)
- Equality Checking for General Type Theories in Andromeda 2 (Q5041060) (← links)
- RustHorn: CHC-Based Verification for Rust Programs (Q5041108) (← links)
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis (Q5048989) (← links)
- A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper) (Q5048990) (← links)
- Deep Generation of Coq Lemma Names Using Elaborated Terms (Q5048996) (← links)
- Validating Mathematical Structures (Q5048998) (← links)
- Formalization of Forcing in Isabelle/ZF (Q5049004) (← links)
- Schemes in Lean (Q5094471) (← links)
- Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types (Q5094472) (← links)
- Formalizing Galois Theory (Q5094476) (← links)
- Elaborating dependent (co)pattern matching: No pattern left behind (Q5110925) (← links)
- MODULARITY IN MATHEMATICS (Q5221289) (← links)
- Implementing type theory in higher order constraint logic programming (Q5236551) (← links)
- Eliminating dependent pattern matching without K (Q5371975) (← links)
