Pages that link to "Item:Q5327343"

The following pages link to A Machine-Checked Proof of the Odd Order Theorem (Q5327343):

Displaying 50 items.

• Recycling proof patterns in Coq: case studies (Q475385) (← links)
• An introduction to mechanized reasoning (Q504394) (← links)
• Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
• A formalization of multi-tape Turing machines (Q744986) (← links)
• Computer-aided proof of Erdős discrepancy properties (Q892235) (← links)
• The role of the Mizar mathematical library for interactive proof development in Mizar (Q1663215) (← links)
• Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
• Automating formalization by statistical and semantic parsing of mathematics (Q1687711) (← links)
• Formalization of the Lindemann-Weierstrass theorem (Q1687717) (← links)
• A formal proof in Coq of Lasalle's invariance principle (Q1687728) (← links)
• Certifying standard and stratified Datalog inference engines in SSReflect (Q1687733) (← links)
• Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
• Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
• Univalence as a principle of logic (Q1788330) (← links)
• Foreword to the special focus on formal proofs for mathematics and computer science (Q2018656) (← links)
• Towards the automatic mathematician (Q2055841) (← links)
• Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem (Q2069874) (← links)
• Experiences from exporting major proof assistant libraries (Q2069875) (← links)
• Formal verification of cP systems using Coq (Q2152300) (← links)
• A library for formalization of linear error-correcting codes (Q2209551) (← links)
• Classification of finite fields with applications (Q2323448) (← links)
• Formalization of universal algebra in Agda (Q2333322) (← links)
• Modelling algebraic structures and morphisms in ACL2 (Q2349534) (← links)
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry (Q2354917) (← links)
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
• A fully automatic theorem prover with human-style output (Q2362206) (← links)
• Deepalgebra -- an outline of a program (Q2364671) (← links)
• Type theory and formalisation of mathematics (Q2399357) (← links)
• From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
• Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge (Q2663667) (← links)
• Reliability of mathematical inference (Q2695405) (← links)
• Congruence Closure in Intensional Type Theory (Q2817913) (← links)
• Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface (Q2945623) (← links)
• Computational Complexity Via Finite Types (Q2946764) (← links)
• Proof Verification Technology and Elementary Physics (Q3296311) (← links)
• Mining the Archive of Formal Proofs (Q3453102) (← links)
• Towards the Formalization of Fractional Calculus in Higher-Order Logic (Q3453127) (← links)
• Computational logic: its origins and applications (Q4559535) (← links)
• Certified Graph View Maintenance with Regular Datalog (Q4559800) (← links)
• An introduction to univalent foundations for mathematicians (Q4684362) (← links)
• A Formalization of Properties of Continuous Functions on Closed Intervals (Q5041063) (← links)
• Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis (Q5048989) (← links)
• Deep Generation of Coq Lemma Names Using Elaborated Terms (Q5048996) (← links)
• Validating Mathematical Structures (Q5048998) (← links)
• Formalizing the Face Lattice of Polyhedra (Q5049001) (← links)
• Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types (Q5094472) (← links)
• Formalizing Galois Theory (Q5094476) (← links)
• Proof Auditing Formalised Mathematics (Q5195266) (← links)
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem (Q5204803) (← links)
• Reshaping the metaphor of proof (Q5204811) (← links)