{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/18477"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/18477","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Contributions to the theory of syntax with bindings and to process algebra","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.\"","abstract_html":""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."","abstract_has_math":false,"creators":["Popescu, Andrei"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Gunter, Elsa L.","Agha, Gul A.","Roşu, Grigore","Felty, Amy"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-01-14T22:52:10Z","date_published":"2011-01-14T22:52:10Z","updated_at":"2026-07-22T22:25:11Z","subjects":["Syntax with Bindings","Lambda Calculus","Coinduction","Theorem proving","Isabelle"],"languages":["en"],"rights":["Copyright 2010 Andrei Popescu"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/18477","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Gunter, Elsa L.","Agha, Gul A.","Roşu, Grigore","Felty, Amy"]},{"key":"dc:creator","label":"Author","values":["Popescu, Andrei"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-01-14T22:52:10Z","2010-12"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Syntax with Bindings","Lambda Calculus","Coinduction","Theorem proving","Isabelle"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2010 Andrei Popescu"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/18477"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["\"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)"]},{"key":"dc:title","label":"Title","values":["Contributions to the theory of syntax with bindings and to process algebra"]}]}],"canonical_facts":{"dc:contributor":["Gunter, Elsa L.","Agha, Gul A.","Roşu, Grigore","Felty, Amy"],"dc:creator":["Popescu, Andrei"],"dc:date":["2011-01-14T22:52:10Z","2010-12"],"dc:description":["\"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)"],"dc:identifier":["http://hdl.handle.net/2142/18477"],"dc:language":["en"],"dc:rights":["Copyright 2010 Andrei Popescu"],"dc:subject":["Syntax with Bindings","Lambda Calculus","Coinduction","Theorem proving","Isabelle"],"dc:title":["Contributions to the theory of syntax with bindings and to process algebra"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:11Z"}