git.iko.soy/Idris-dev
on b8a2bbf help sign in
Idris-dev/impl-paper/impldtp.tex
107 lines 2.6 kB history raw
1%\documentclass{llncs}
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}}
51\markboth{Edwin C. Brady}{Implementation of a Practical Dependently
52 Typed Functional Programming Language}
53\title{Implementation of a Practical Dependently Typed Functional
54 Programming Language}
55\author{EDWIN C. BRADY\\ University of St Andrews}
57\begin{abstract}
58I describe the implementation of a dependently typed functional
59programming language, \Idris{}. Much has been written about various
60aspects of dependently typed language implementation (e.g. checking
61dependent types, unification, optimisation) but nothing yet about how
62to bring it all together into a complete, practical, usable tool. This paper
63attempts to do so. In particular, I explain what is needed to turn
64concrete syntax with implicit arguments into fully elaborated type
65theory, using unification and a tactic engine.
66\end{abstract}
68\category{D.3.2}{Programming Languages}{Language
69 Classifications}[Applicative (functional) Languages]
70\category{D.3.4}{Programming Languages}{Processors}[Compilers]
71\terms{Languages, Verification, Performance}
72\keywords{Dependent Types, Typechecking}
74\begin{document}
76\begin{bottomstuff}
77Author's address: Edwin Brady, School of Computer Science, North Haugh, St Andrews,
78KY16 9SX
79\end{bottomstuff}
80\maketitle
82\input{intro.tex}
84\input{overview.tex}
86\input{hll.tex}
88\input{typechecking.tex}
90\input{proofstate.tex}
92\input{elaboration.tex}
94\input{compiling.tex}
96\input{syntax.tex}
98\input{conclusions.tex}
100\bibliographystyle{acmtrans}
101\bibliography{literature.bib}
103\appendix
105%\input{code}
107\end{document}