Contributions to the theory of syntax with bindings and to process algebra

Syntax with Bindings;Lambda Calculus;Coinduction;Theorem proving;Isabelle

Popescu, Andrei

关键词: Syntax with Bindings;    Lambda Calculus;    Coinduction;    Theorem proving;    Isabelle;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/18477/Popescu_Andrei.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

We develop a theory of syntax with bindings, focusing on:- methodological issues concerning the convenient representation of syntax;- techniques for recursive definitions and inductive reasoning.Our approach consists of a combination of FOAS (First-Order Abstract Syntax) and HOAS (Higher-Order Abstract Syntax) and tries to take advantage of the best of both worlds.The connection between FOAS and HOAS follows some general patterns and is presented as a (formally certified) statement of adequacy.We also develop a general technique for proving bisimilarity in process algebra. Our technique, presented as a formal proof system, is applicable to a wide range of process algebras.The proof system is incremental,in that it allows building incrementally an a priori unknownbisimulation, and pattern-based, in that it works on equalities of process patterns (i.e., universally quantified equations of process terms containing process variables), thus taking advantage of equational reasoningin a "circular" manner, inside coinductive proof loops.All the work presented here has been formalized in the Isabelle theorem prover. The formalization is performed in a general setting: arbitrary many-sorted syntax with bindings and arbitrary SOS-specified process algebra in de Simone format. The usefulness of our techniques is illustrated by several formalized case studies:- a development of call-by-name and call-by-value lambda-calculus with constants, includingChurch-Rosser theorems, connection with de Bruijn representation,connection with other Isabelle formalizations, HOAS representation, and contituation-passing-style (CPS) transformation;- a proof in HOAS of strong normalization for the polymorphic second-order lambda-calculus (a.k.a. System F).We also indicate the outline and some details of the formal development.