Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the π-Calculus and Mechanizing the Theory of Contexts.
In: Foundations of Software Science & Computation Structures (978-3-540-41864-1); 2001, p364-378, 15p
Buch
Zugriff:
Higher-order abstract syntax is a natural way to formalize programming languages with binders, like the π-calculus, because α-conversion, instantiations and capture avoidance are delegated to the meta-level of the provers, making tedious substitutions superfluous. However, such formalizations usually lack structural induction, which makes syntax-analysis impossible. Moreover, when applied in logical frameworks with object-logics, like Isabelle/HOL or standard extensions of Coq, exotic terms can be defined, for which important syntactic properties become invalid. The paper presents a formalization of the π-calculus in Isabelle/HOL, using well-formedness predicates which both eliminate exotic terms and yield structural induction. These induction-principles are then used to derive the Theory of Contexts fully within the mechanization. [ABSTRACT FROM AUTHOR]
Copyright of Foundations of Software Science & Computation Structures (978-3-540-41864-1) is the property of Springer eBooks and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Titel: |
Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the π-Calculus and Mechanizing the Theory of Contexts.
|
---|---|
Autor/in / Beteiligte Person: | Goos, Gerhard ; Hartmanis, Juris ; van Leeuwen, Jan ; Honsell, Furio ; Miculan, Marino ; Röckl, Christine ; Hirschkoff, Daniel ; Berghofer, Stefan |
Quelle: | Foundations of Software Science & Computation Structures (978-3-540-41864-1); 2001, p364-378, 15p |
Veröffentlichung: | 2001 |
Medientyp: | Buch |
ISBN: | 978-3-540-41864-1 (print) |
DOI: | 10.1007/3-540-45315-6_24 |
Sonstiges: |
|