Ivor, a Proof Engine

DOI10.1007/978-3-540-74130-5_9MaRDI QIDQ3612951zbMATH OpenOpenAlexFDO

Authors Edwin Brady

Publication date 11 March 2009

Published in Implementation and Application of Functional Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-74130-5_9

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 140008
• Java: Embedding a programming language in a theorem prover
• The Lean theorem prover (system description)
• Dependent types ensure partial correctness of theorem provers
• A Brief Overview of Agda – A Functional Language with Dependent Types

Cited in

(1)

• Ivor

Describes a project that uses

Uses Software

• Coq
• CLEAN
• Isabelle/HOL
• Haskell
• Why3
• LEGO
• Agda
• Hume

This page was built for publication: Ivor, a Proof Engine

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3612951)