Files in this item

FilesDescriptionFormat

application/pdf

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

Description

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
Degree:Ph.D.
Genre:Dissertation
Subject(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.
Issue Date:2011-01-14
URI:http://hdl.handle.net/2142/18477
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