Recent Changes - Search:

FP


The Chalmers FP wiki is part of the CSE dept. wiki.

Recent Changes


edit SideBar

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

Contact

Patrik Jansson

Edit - History - Print - Recent Changes - Search
Page last modified on March 16, 2015, at 01:16 PM