Formalising Mathematics in Simple Type Theory

DOI10.1007/978-3-030-15655-8_20zbMath1528.03098arXiv1804.07860OpenAlexW2798940414MaRDI QIDQ6075439

Lawrence Charles Paulson

Publication date: 20 September 2023

Published in: Synthese Library (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1804.07860

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Partial and nested recursive function definitions in higher-order logic
• Constructing recursion operators in intuitionistic type theory
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• Organizing numerical theories using axiomatic type classes
• A compendium of continuous lattices in MIZAR
• Coquelicot: a user-friendly library of real analysis for Coq
• Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
• Formalizing an analytic proof of the prime number theorem
• Formalization of the Resolution Calculus for First-Order Logic
• Truly Modular (Co)datatypes for Isabelle/HOL
• A Consistent Foundation for Isabelle/HOL
• A Brief Overview of Agda – A Functional Language with Dependent Types
• The Four Colour Theorem: Engineering of a Formal Proof
• Logic and Computation
• Mechanizing coinduction and corecursion in higher-order logic
• Computational logic: its origins and applications
• Natural deduction as higher-order resolution
• Scalable LCF-Style Proof Translation
• A Machine-Checked Proof of the Odd Order Theorem
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Theorem Proving in Higher Order Logics
• Formalization of the fundamental group in untyped set theory using auto2

This page was built for publication: Formalising Mathematics in Simple Type Theory