Semantics Engineering with Concrete Syntax and Theorem Proving
| Název práce v češtině: | Semantics Engineering with Concrete Syntax and Theorem Proving |
|---|---|
| Název v anglickém jazyce: | Semantics Engineering with Concrete Syntax and Theorem Proving |
| Klíčová slova: | semantics engineering|programming language theory|concrete syntax|theorem proving |
| Akademický rok vypsání: | 2023/2024 |
| Typ práce: | disertační práce |
| Jazyk práce: | čeština |
| Ústav: | Katedra distribuovaných a spolehlivých systémů (32-KDSS) |
| Vedoucí / školitel: | Mgr. Tomáš Petříček, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 28.02.2024 |
| Datum zadání: | 28.02.2024 |
| Datum potvrzení stud. oddělením: | 05.03.2024 |
| Zásady pro vypracování |
| 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]. |
| Seznam odborné literatury |
| [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. |