| dc.contributor.author | Ekici, Burak | |
| dc.date.accessioned | 2023-02-07T11:04:33Z | |
| dc.date.available | 2023-02-07T11:04:33Z | |
| dc.date.issued | 2023 | en_US |
| dc.identifier.citation | Ekici, B. A Sound Definitional Interpreter for a Simply Typed Functional Language. Axioms 2023, 12, 43. https://doi.org/ 10.3390/axioms12010043 | en_US |
| dc.identifier.issn | 20751680 | |
| dc.identifier.uri | https://doi.org/ 10.3390/axioms12010043 | |
| dc.identifier.uri | https://hdl.handle.net/20.500.12809/10515 | |
| dc.description.abstract | In this paper, we develop, in the proof assistant Coq, a definitional interpreter and a type-checker for a simply typed functional language, and formally prove that the mentioned type-checker is sound with respect to the definitional interpreter via progress and preservation. To represent binders, we embark on the choice of “concrete syntax” in which parameters are just names (or strings). | en_US |
| dc.item-language.iso | eng | en_US |
| dc.publisher | MDPI | en_US |
| dc.relation.isversionof | 10.3390/axioms12010043 | en_US |
| dc.item-rights | info:eu-repo/semantics/openAccess | en_US |
| dc.subject | Definitional interpreters | en_US |
| dc.subject | Simply typed functional languages | en_US |
| dc.subject | Formal soundness proofs | en_US |
| dc.subject | The Coq proof assistant | en_US |
| dc.title | A Sound Definitional Interpreter for a Simply Typed Functional Language | en_US |
| dc.item-type | article | en_US |
| dc.contributor.department | MÜ, Mühendislik Fakültesi, Bilgisayar Mühendisliği Bölümü | en_US |
| dc.contributor.authorID | 0000-0002-6602-7906 | en_US |
| dc.contributor.institutionauthor | Ekici, Burak | |
| dc.identifier.volume | 12 | en_US |
| dc.identifier.issue | 1 | en_US |
| dc.relation.journal | Axioms | en_US |
| dc.relation.publicationcategory | Makale - Uluslararası Hakemli Dergi - Kurum Öğretim Elemanı | en_US |
