Second-Order Programs with Preconditions

DOI10.1007/978-3-642-17172-7_8zbMath1309.68035OpenAlexW1602965671MaRDI QIDQ3058455

Markus Aderhold

Publication date: 22 November 2010

Published in: Verification, Induction, Termination Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-17172-7_8

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• ACL2
• Isabelle/HOL
• Haskell
• Eiffel
• Spec#
• ETPS
• VeriFun

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• An introduction to mathematical logic and type theory: To truth through proof.
• Context Dependent Procedures and Computed Types in ✓eriFun
• Static contract checking for Haskell
• Reasoning About Incompletely Defined Programs
• Meta Reasoning in ACL2
• Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Second-Order Programs with Preconditions