Files in this item



application/pdfPopescu_Andrei.pdf (1MB)
(no description provided)PDF


Title:Contributions to the theory of syntax with bindings and to process algebra
Author(s):Popescu, Andrei
Director of Research:Gunter, Elsa L.
Doctoral Committee Chair(s):Gunter, Elsa L.
Doctoral Committee Member(s):Agha, Gul A.; Roşu, Grigore; Felty, Amy
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Syntax with Bindings
Lambda Calculus
Theorem proving
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.
Issue Date:2011-01-14
Rights Information:Copyright 2010 Andrei Popescu
Date Available in IDEALS:2011-01-14
Date Deposited:2010-12

This item appears in the following Collection(s)

Item Statistics