Pages that link to "Item:Q3454108"
From MaRDI portal
The following pages link to The Lean Theorem Prover (System Description) (Q3454108):
Displaying 27 items.
- Implementing type theory in higher order constraint logic programming (Q5236551) (← links)
- Eliminating dependent pattern matching without K (Q5371975) (← links)
- System Description: The Proof Transformation System CERES (Q5747781) (← links)
- (Q5875411) (← links)
- (Q5875427) (← links)
- (Q5875441) (← links)
- Verified Decision Procedures for Modal Logics. (Q5875443) (← links)
- Declarative Proof Translation (Short Paper) (Q5875449) (← links)
- Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck} (Q5919026) (← links)
- Validating safety arguments with Lean (Q6041273) (← links)
- Fundamentals of compositional rewriting theory (Q6052944) (← links)
- What is the point of computers? A question for pure mathematicians (Q6118162) (← links)
- Abstraction boundaries and spec driven development in pure mathematics (Q6130524) (← links)
- Certifying expressive power and algorithms of reversible primitive permutations with \textsf{Lean} (Q6151610) (← links)
- A formalization of the change of variables formula for integrals in mathlib (Q6159362) (← links)
- Formalising the Kruskal-Katona theorem in Lean (Q6159369) (← links)
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction (Q6487292) (← links)
- Satisfiability modulo finite fields (Q6535532) (← links)
- Verified reductions for optimization (Q6536123) (← links)
- Computing with the universal properties of the Clifford algebra and the even subalgebra (Q6550515) (← links)
- Automated deduction (Q6602250) (← links)
- One or nothing: anti-unification over the simply-typed lambda calculus (Q6610194) (← links)
- Algorithm and abstraction in formal mathematics (Q6637783) (← links)
- A formalization of all notions in the statement of a theorem by Deligne (Q6648157) (← links)
- Incorporating a database of graphs into a proof assistant (Q6648164) (← links)
- On the Erdős-Tuza-Valtr conjecture (Q6655707) (← links)
- HepLean: digitalising high energy physics (Q6671943) (← links)
