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

"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 unknown bisimulation, 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 reasoning in 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, including Church-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."

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2011

Author dc:creator

• Popescu, Andrei

Contributors dc:contributor

• Gunter, Elsa L.
• Agha, Gul A.
• Roşu, Grigore
• Felty, Amy

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

Statement dc:rights

• Copyright 2010 Andrei Popescu

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/18477

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/18477