Abstract
In this thesis we give an algebraic characterization of the syntax and semantics of simply–typed languages. More precisely, we characterize simply–typed binding syntax equipped with reduction rules via a universal property, namely as the initial object of some category.
We specify a language by a 2–signature (Σ, A), that is, a signature on two levels: the syntactic level Σ specifies the sorts and terms of the language, and associates a sort to each term. The semantic level A specifies, through inequations, reduction rules on the terms of the language. To any given 2–signature (Σ, A) we associate a category of “models” of (Σ, A). We prove that this category has an initial object, which integrates the terms freely generated by Σ and the reduction relation — on those terms — generated
by A. We call this object the programming language generated by (Σ, A).
Initiality provides an iteration principle which allows to specify translations on the syntax, possibly to a language over different sorts. Furthermore, translations specified via the iteration principle are by construction type–safe and faithful with respect to reduction.
To illustrate our results, we consider two examples extensively: firstly, we specify a double negation translation from classical to intuitionistic propositional logic via the category–theoretic iteration principle. Secondly, we specify a translation from PCF to the untyped lambda calculus which is faithful with respect to reduction in the source and
target languages.
In a second part, we formalize some of our initiality theorems in the proof assistant Coq. The implementation yields a machinery which, when given a 2–signature, returns an implementation of its associated abstract syntax together with certified substitution operation, iteration operator and a reduction relation generated by the specified reduction rules.
We specify a language by a 2–signature (Σ, A), that is, a signature on two levels: the syntactic level Σ specifies the sorts and terms of the language, and associates a sort to each term. The semantic level A specifies, through inequations, reduction rules on the terms of the language. To any given 2–signature (Σ, A) we associate a category of “models” of (Σ, A). We prove that this category has an initial object, which integrates the terms freely generated by Σ and the reduction relation — on those terms — generated
by A. We call this object the programming language generated by (Σ, A).
Initiality provides an iteration principle which allows to specify translations on the syntax, possibly to a language over different sorts. Furthermore, translations specified via the iteration principle are by construction type–safe and faithful with respect to reduction.
To illustrate our results, we consider two examples extensively: firstly, we specify a double negation translation from classical to intuitionistic propositional logic via the category–theoretic iteration principle. Secondly, we specify a translation from PCF to the untyped lambda calculus which is faithful with respect to reduction in the source and
target languages.
In a second part, we formalize some of our initiality theorems in the proof assistant Coq. The implementation yields a machinery which, when given a 2–signature, returns an implementation of its associated abstract syntax together with certified substitution operation, iteration operator and a reduction relation generated by the specified reduction rules.
Original language | English |
---|---|
Number of pages | 155 |
Journal | Journal of Formalized Reasoning |
Volume | 8 |
Issue number | 2 |
DOIs | |
Publication status | Published - 2015 |
Bibliographical note
Special Issue - PhD ThesisKeywords
- relative monads
- Coq
- initial semantics
ASJC Scopus subject areas
- Mathematics(all)