FP /
AgdaBackendForOTT
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.
Prerequisites:
Logic in Computer Science, Types for programs and proofs, Functional Programming, Programming Languages, Compiler Construction