Towards a Formally Verified Proof Assistant

DOI10.1007/978-3-319-08970-6_3zbMath1416.68146OpenAlexW2166178233MaRDI QIDQ2879241

Abhishek Anand, Vincent Rahli

Publication date: 8 September 2014

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: http://pure-oai.bham.ac.uk/ws/files/71147559/Towards_a_Formally_Verified.pdf

Mathematics Subject Classification ID

Related Items (9)

Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ A Consistent Foundation for Isabelle/HOL ⋮ A consistent foundation for Isabelle/HOL ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Cartesian cubical computational type theory: Constructive reasoning with paths and equalities ⋮ Exercising Nuprl’s Open-Endedness ⋮ \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic ⋮ Formally computing with the non-computable

Uses Software

• Coq
• Isabelle/HOL
• HOL Light
• Nuprl
• CakeML
• Agda
• Milawa
• Paco
• Jitawa

This page was built for publication: Towards a Formally Verified Proof Assistant