FP /


Agda-backend for OTT

OTT is a tool for writing definitions of programming languages and calculi. It takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle versions of the definition. The goal of this project is to extend OTT with a backend for generating Agda code.

Agda is a dependently typed programming language with good support for programming with inductively defined families of types.


Logic in Computer Science, Types for programs and proofs, Functional Programming, Programming Languages, Compiler Construction


Patrik Jansson