A pluralist approach to the formalisation of mathematics

DOI10.1017/S0960129511000156zbMath1242.03027OpenAlexW2026761730MaRDI QIDQ3094181

Robin Adams, Zhaohui Luo

Publication date: 21 October 2011

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129511000156

zbMATH Keywords

type theorylogical frameworkformalisation of mathematicsproof reuse

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Uses Software

• Coq
• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The system \({\mathcal F}\) of variable types, fifteen years later
• The calculus of constructions
• The Russell–Prawitz modality
• Weyl's predicative classical mathematics as a logic-enriched type theory
• Formalising foundations of mathematics
• Packaging Mathematical Structures
• Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory
• The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
• A framework for defining logics
• PAL⁺: a lambda-free logical framework
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
• The generalised type-theoretic interpretation of constructive set theory
• An implementation of LF with coercive subtyping and universes

This page was built for publication: A pluralist approach to the formalisation of mathematics