git.iko.soy/Idris-dev
on 42dcbab help sign in
Idris-dev/impl-paper/impldtp.tex
113 lines 2.8 kB history raw
1\documentclass{jfp1}
2%\documentclass[acmtoplas]{acmtrans2m}
4\usepackage[draft]{comments}
5%\usepackage[final]{comments}
6% \newcommand{\comment}[2]{[#1: #2]}
7\newcommand{\khcomment}[1]{\comment{KH}{#1}}
8\newcommand{\ebcomment}[1]{\comment{EB}{#1}}
10\usepackage{epsfig}
11%\usepackage{path}
12\usepackage{url}
13%\usepackage{amsmath,amssymb}
14\usepackage{fancyvrb}
16\newenvironment{template}{\sffamily}
18\usepackage{graphics,epsfig}
19\usepackage{stmaryrd}
21\input{./macros.ltx}
22\input{./library.ltx}
24\NatPackage
25\FinPackage
27\newcounter{per}
28\setcounter{per}{1}
30\newcommand{\Ivor}{\textsc{Ivor}}
31\newcommand{\Idris}{\textsc{Idris}}
32\newcommand{\Funl}{\textsc{Funl}}
33\newcommand{\Agda}{\textsc{Agda}}
34\newcommand{\LamPi}{$\lambda_\Pi$}
36\newcommand{\perule}[1]{\vspace*{0.1cm}\noindent
37\begin{center}
38\fbox{
39\begin{minipage}{7.5cm}\textbf{Rule \theper:} #1\addtocounter{per}{1}
40\end{minipage}}
41\end{center}
42\vspace*{0.1cm}
45\newcommand{\mysubsubsection}[1]{
46\noindent
47\textbf{#1}
49\newcommand{\hdecl}[1]{\texttt{#1}}
52\title[Implementation of a Practical Functional Language with Dependent Types]
53 {Implementation of a Practical Functional Programming Language with Dependent Types}
54%\subtitle{Implementing Domain Specific Languages by Overloading}
56\author[Edwin Brady]
57{EDWIN BRADY\\
58School of Computer Science, University of St Andrews, St Andrews,
59KY16 9SX, UK}
61\begin{document}
63\maketitle
65\begin{abstract}
66I describe the implementation of a dependently typed functional
67programming language, \Idris{}. Much has been written about various
68aspects of dependently typed language implementation (e.g. checking
69dependent types, unification, optimisation) but nothing yet about how
70to bring it all together into a complete, practical, usable tool. This paper
71attempts to do so. In particular, I explain what is needed to turn
72concrete syntax with implicit arguments into fully elaborated type
73theory, using unification and a tactic engine.
74\end{abstract}
76%\category{D.3.2}{Programming Languages}{Language
77% Classifications}[Applicative (functional) Languages]
78%\category{D.3.4}{Programming Languages}{Processors}[Compilers]
79%\terms{Languages, Verification, Performance}
80%\keywords{Dependent Types, Typechecking}
83%\begin{bottomstuff}
84%Author's address: Edwin Brady, School of Computer Science, North Haugh, St Andrews,
85%KY16 9SX
86%\end{bottomstuff}
88\input{intro.tex}
90\input{overview.tex}
92\input{hll.tex}
94\input{typechecking.tex}
96\input{proofstate.tex}
98\input{elaboration.tex}
100\input{compiling.tex}
102\input{syntax.tex}
104\input{conclusions.tex}
106\bibliographystyle{jfp}
107\bibliography{library.bib}
109\appendix
111%\input{code}
113\end{document}