Barendregt’s Variable Convention in Rule Inductions

DOI10.1007/978-3-540-73595-3_4MaRDI QIDQ3608761zbMATH OpenOpenAlexFDO

Authors Christian Urban, Stefan Berghofer, Michael Norrish

Publication date 6 March 2009

Published in Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73595-3_4

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Nominal Inversion Principles
• Formalised Inductive Reasoning in the Logic of Bunched Implications
• Automated Deduction – CADE-20
• Engineering formal metatheory
• scientific article; zbMATH DE number 4014064

Cited in

(18)

• A formalized general theory of syntax with bindings
• A solution to the PoplMark challenge based on de Bruijn indices
• A formalized general theory of syntax with bindings: extended version
• Rensets and renaming-based recursion for syntax with bindings
• A canonical locally named representation of binding
• Formalizing adequacy: a case study for higher-order abstract syntax
• On the role of names in reasoning about -tree syntax specifications
• Mechanizing the metatheory of mini-XQuery
• The role of indirections in lazy natural semantics
• Nominal Inversion Principles
• Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
• Psi-calculi in Isabelle
• Psi-calculi in Isabelle
• Rensets and renaming-based recursion for syntax with bindings extended version
• Invertibility in Sequent Calculi
• Strong Normalization of Moggis's Computational Metalanguage
• Nominal techniques in Isabelle/HOL
• External and internal syntax of the \(\lambda \)-calculus

Describes a project that uses

Uses Software

• Isar

This page was built for publication: Barendregt’s Variable Convention in Rule Inductions

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