2026-09-19T11:15:21Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/18477 2023-07-10 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Gunter, Elsa L. Gunter, Elsa L. Agha, Gul A. Roşu, Grigore Felty, Amy Popescu, Andrei 2011-01-14T22:52:10Z 2011-01-14T22:52:10Z 2011-01-14T22:52:10Z 2010-12 "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." Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2010-12-01T16:34:36Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 thesisAtUIUC.zip: 22571475 bytes, checksum: 98e1a17e518e67f28392c700a0422e16 (MD5) Popescu_Andrei.pdf: 1369855 bytes, checksum: ab524029096e6e39cafe6f5bcb2bcb2f (MD5) Made available in DSpace on 2011-01-14T22:52:10Z (GMT). No. of bitstreams: 3 Popescu_Andrei.pdf: 1369855 bytes, checksum: ab524029096e6e39cafe6f5bcb2bcb2f (MD5) license.txt: 4064 bytes, checksum: 66a4175d4edb5fd896e5e52ce40c34ec (MD5) thesisAtUIUC.zip: 22571475 bytes, checksum: 98e1a17e518e67f28392c700a0422e16 (MD5) http://hdl.handle.net/2142/18477 en Copyright 2010 Andrei Popescu Syntax with Bindings Lambda Calculus Coinduction Theorem proving Isabelle Contributions to the theory of syntax with bindings and to process algebra Computer Science 1434 Computer Science 0112 University of Illinois at Urbana-Champaign Dissertation Ph.D. PHD:Computer Science -UIUC 10KS0112PHD