Semantics Engineering with Concrete Syntax and Theorem Proving
| Thesis title in Czech: | Semantics Engineering with Concrete Syntax and Theorem Proving |
|---|---|
| Thesis title in English: | Semantics Engineering with Concrete Syntax and Theorem Proving |
| Key words: | semantics engineering|programming language theory|concrete syntax|theorem proving |
| Academic year of topic announcement: | 2023/2024 |
| Thesis type: | dissertation |
| Thesis language: | čeština |
| Department: | Department of Distributed and Dependable Systems (32-KDSS) |
| Supervisor: | Mgr. Tomáš Petříček, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 28.02.2024 |
| Date of assignment: | 28.02.2024 |
| Confirmed by Study dept. on: | 05.03.2024 |
| Guidelines |
| In programming language research, formal semantics is a crucial tool for formally describing programming languages and systems and studying their properties. Formal semantics is increasingly constructed using semantics engineering tools such as PLT Redex [1] and proves about formal semantics are increasingly verified using theorem providers such as Coq and Agda [4, 5]. This thesis will investigate ways of bringing those two kinds of tools together. It will take as the starting point semantics engineering tools such as PLT Redex and Lambdulus [1, 3], but propose novel ways of (1) integrating theorem proving directly into the process of defining and exploring programming language semantics and (2) building semantics for languages with concrete syntax as inspired, e.g., by [2]. |
| References |
| [1] Felleisen, Matthias, Robert Bruce Findler, and Matthew Flatt. Semantics engineering with PLT Redex. MIT Press, 2009.
[2] van der Storm, Tijs. "Semantics Engineering with Concrete Syntax." Eelco Visser Commemorative Symposium (EVCS 2023). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2023. [3] Sliacky, Jan, and Petr Maj. "Lambdulus: teaching lambda calculus practically." Proceedings of the 2019 ACM SIGPLAN Symposium on SPLASH-E. 2019. [4] Wadler, Philip, Wen Kokke, and Jeremy G. Siek. Programming Language Foundations in Agda. Available at https://plfa.inf.ed.ac.uk/22.08/. 2022. [5] Chlipala, Adam. Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant. MIT Press, 2022. |