Instituto de Computación
Universidad de la República, Montevideo
Thursday, 9 June 2016, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: One common approach to formal compiler construction is to first write the compiler, having in mind in that process the semantics of the involved languages, and then, as a second step, perform the proof of correctness of that compiler. This approach is known as externalist and has been investigated in different formal settings such as formal specification methods (in particular algebraic ones), categorical formalisations of programming languages, dependently-typed languages, etc. In this talk, we present preliminary results of on-going work on an alternative approach to compiler construction that follows an internalist discipline. This means that we develop simultaneously the compiler and its correctness proof. Our development is performed in Agda. The idea is to decorate the data types that model the abstract syntax of each language with the semantics description of that language and write the compiler between those decorated types. That way, compiler correctness reduces to type-correctness. Modulo minor details, the texts of the compiler and its proof are almost the same. We show the translations between a simple while language and a semi-structured code for a stack machine. Although we do not use that framework, our approach has similarities with McBride's ornaments.
This is joint work with Emmanuel Gunther, Miguel Pagano and Marcos Viera.