back to main page

Work done by Benedikt Ahrens

Publications

• Modules over relative monads for syntax and semantics
  arXiv:1107.5252 [cs.LO]
  To be published in Math. Struc. in Comp. Science
  A theorem about initiality of syntax equipped with a reduction relation. Syntax is modelled as a relative monad.
• Extended Initiality for Typed Abstract Syntax
  Logical Methods in Computer Science, Vol. 8, No. 2 (2012)
  arXiv:1107.4751 [cs.LO]
  A theorem allowing us to consider the translation between two languages typed over different sets of types as an initial morphism in some category.
• with J. Zsidó: Initial Semantics for higher-order typed syntax in Coq
  Journal of Formalized Reasoning, Vol. 4, No. 1 (2011)

bibtex entries

Code

In my PhD thesis I formalize the semantics of functional languages in a categorical setting in the proof assistant Coq. The goal is hence twofold:

• develop a library of category theory for general purpose
• use the library to prove some results about categorical syntax & semantics

The latest version of the library can be viewed here -- see also the description file DESCRIPTION (txt) -- and downloaded using
$ fossil clone http://web.math.unifi.it/~benedikt/r.cgi/coq coq.fossil
$ fossil open coq.fossil
Alternatively, it can be downloaded as a ZIP archive from the web page after anonymous login (Timeline -> Leaf -> ZIP archive).

back to main page