Nominal Inversion Principles

DOI10.1007/978-3-540-71067-7_10MaRDI QIDQ3543650zbMATH OpenOpenAlexFDO

Authors Stefan Berghofer, Christian Urban

Publication date 4 December 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71067-7_10

Mathematics Subject Classification ID

Recommendations

• Automating inversion of inductive predicates in Coq
• Barendregt’s Variable Convention in Rule Inductions
• Automated Deduction – CADE-20
• Engineering formal metatheory
• Alpha-structural induction and recursion for the lambda calculus in constructive type theory

Cites work

• Automated Deduction – CADE-20
• Barendregt’s Variable Convention in Rule Inductions
• Engineering formal metatheory
• Nominal logic, a first order theory of names and binding
• Theorem Proving in Higher Order Logics

Cited in

(10)

• A canonical locally named representation of binding
• Mechanizing the metatheory of mini-XQuery
• On Inversion Principles
• Barendregt’s Variable Convention in Rule Inductions
• INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES
• Automating inversion of inductive predicates in Coq
• Formal SOS-Proofs for the Lambda-Calculus
• Handcrafted inversions made operational on operational semantics
• Psi-calculi in Isabelle
• Psi-calculi in Isabelle

Describes a project that uses

Uses Software

• PoplMark
• Nominal Isabelle

This page was built for publication: Nominal Inversion Principles

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