K-user mailing list

[Andrej Tokarčík <andrejtokarcik AT gmail.com>]

Dear K users and developers,

I would like to inform you of my master's thesis entitled "An
Executable Formal Semantics of Agda" finished in June of this year. It
implements a partial semantics of the dependently typed programming
language Agda (in its 2.4.2.2 version in particular) using the K
framework 3.4. The project was inspired by a GSoC idea [1] and to the
best of my knowledge it is the first dependently typed language
defined in K as well as the first attempt to formalise the semantics
of the Agda language as such (rather than a 'core type theory').

Perhaps the most important part of the text [2] is the appendix that
explains the technical details pertaining to how to use the auxiliary
scripts and understand the output. The actual K code resides in the
Git repository at [3].

Currently I have no plans to continue with the work in order to extend
the covered functionality. Anyway, I hope even in its current state it
may be of some use to the K community.

All the best,
Andrej Tokarčík

[1] 
http://www.kframework.org/index.php/ProjectIdeas#Define_an_existing_language
[2] http://is.muni.cz/th/373877/fi_m/?lang=en
[3] https://github.com/andrejtokarcik/agda-semantics