K-user mailing list

["Moore, Brandon Michael" <bmmoore AT illinois.edu>]

That's very interesting.

The incomplete features probably prevented you from compiling any of the 
standard library or larger programs, unfortunately.
Did you notice any problems from relying on K's unification module rather 
than replicating Agda's meta inference exactly? From trying Agda myself I 
notice it seems to solve some pretty fancy higher-order unification problems 
if necesssary.

Would you like us to include this semantics in the official K repository at 
https://github.com/kframework ?

If so, we would be happy to add it if you can add license giving us 
permission.
For example, the two semantics started by David have an MIT license.
The C semantics is under the same University of Illinois/NCSA license as K 
itself.
It's roughly equivalent, just less well known).

Brandon
________________________________________
From: Andrej Tokarčík 
[andrejtokarcik AT gmail.com]
Sent: Monday, August 10, 2015 6:19 AM
To: 
k-user AT cs.uiuc.edu
Subject: [[K-user] ] An Agda semantics

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