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

Popescu, Andrei

Permalink

https://hdl.handle.net/2142/18477 Copy

Description

Title

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

Author(s)

Popescu, Andrei

Issue Date

2011-01-14T22:52:10Z

Director of Research (if dissertation) or Advisor (if thesis)

Gunter, Elsa L.

Doctoral Committee Chair(s)

Gunter, Elsa L.

Committee Member(s)

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

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

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

Abstract

"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."

Graduation Semester

2010-12

Permalink

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

Copyright and License Information

Copyright 2010 Andrei Popescu

Owning Collections