Programming Inductive Proofs

DOI10.1007/978-3-642-17172-7_1zbMath1309.68051OpenAlexW197201650MaRDI QIDQ3058448

Brigitte Pientka

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_1

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Unnamed Item ⋮ Harpoon: mechanizing metatheory interactively ⋮ Rensets and renaming-based recursion for syntax with bindings

Uses Software

• Beluga
• Twelf
• Abella
• PoplMark
• Elf
• Delphin

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verifying termination and reduction properties about higher-order logic programs
• A formally verified compiler back-end
• Case Analysis of Higher-Order Data
• Towards a mechanized metatheory of standard ML
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
• The Abella Interactive Theorem Prover (System Description)
• A framework for defining logics
• Explicit substitutions
• A verified compiler for an impure functional language
• Contextual modal type theory
• Theorem Proving in Higher Order Logics
• Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

This page was built for publication: Programming Inductive Proofs