Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
From MaRDI portal
Publication:2945649
DOI10.1007/978-3-319-22102-1_24zbMath1465.68037OpenAlexW2402209726MaRDI QIDQ2945649
Tobias Tebbi, Gert Smolka, Steven Schäfer
Publication date: 14 September 2015
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-22102-1_24
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)
Related Items (9)
Tower Induction and Up-to Techniques for CCS with Fixed Points ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Variable binding and substitution for (nameless) dummies ⋮ Variable binding and substitution for (nameless) dummies ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Rensets and renaming-based recursion for syntax with bindings
Uses Software
This page was built for publication: Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
