Barendregt’s Variable Convention in Rule Inductions
From MaRDI portal
Publication:3608761
DOI10.1007/978-3-540-73595-3_4zbMath1213.03024OpenAlexW2113705064MaRDI QIDQ3608761
Stefan Berghofer, Christian Urban, 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
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Related Items
The Role of Indirections in Lazy Natural Semantics, A canonical locally named representation of binding, Formalizing adequacy: a case study for higher-order abstract syntax, A formalized general theory of syntax with bindings, Rensets and renaming-based recursion for syntax with bindings extended version, A solution to the PoplMark challenge based on de Bruijn indices, Psi-calculi in Isabelle, Psi-calculi in Isabelle, Nominal techniques in Isabelle/HOL, Nominal Inversion Principles, A formalized general theory of syntax with bindings: extended version, External and internal syntax of the \(\lambda \)-calculus, On the Role of Names in Reasoning about λ-tree Syntax Specifications, Mechanizing the Metatheory of mini-XQuery, Rensets and renaming-based recursion for syntax with bindings, Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
Uses Software
