Towards a formally verified proof assistant
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 4053566
- A verified theorem prover backend supported by a monotonic library
- scientific article; zbMATH DE number 1301729
- Formal program optimization in Nuprl using computational equivalence and partial types
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
Cited in
(26)- Formal proof of a machine closed theorem in Coq
- A consistent foundation for Isabelle/HOL
- \(\mathrm{HO}\pi\) in Coq
- Integration of formal proof into unified assurance cases with Isabelle/SACM
- Formally computing with the non-computable
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
- Formal verification for non-formalists
- Exercising Nuprl's open-endedness
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- A consistent foundation for Isabelle/HOL
- Proof assistants for natural language semantics
- Mining the Archive of Formal Proofs
- scientific article; zbMATH DE number 4053566 (Why is no real title available?)
- Validating Brouwer's continuity principle for numbers using named exceptions
- Building reliable, high-performance networks with the Nuprl proof development system
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Towards Formal Proof Script Refactoring
- A verified theorem prover backend supported by a monotonic library
- Formal program optimization in Nuprl using computational equivalence and partial types
- Cooperative Repositories for Formal Proofs
- Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
- \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity
- Open bar -- a Brouwerian intuitionistic logic with a pinch of excluded middle
- Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
- Candle: a verified implementation of HOL Light (extended version)
- A mechanised semantics for HOL with ad-hoc overloading
This page was built for publication: Towards a formally verified proof assistant
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879241)
