Permalink
Browse files

Revision of impl-paper completed.

  • Loading branch information...
1 parent 091a5df commit 296588f31d308b5d754b6821522813ba1e7d4148 @edwinb committed Feb 15, 2013
Showing with 31 additions and 26 deletions.
  1. +7 −5 papers/impl-paper/conclusions.tex
  2. +2 −2 papers/impl-paper/elaboration.tex
  3. +22 −19 papers/impl-paper/library.bib
@@ -2,7 +2,7 @@ \section{Related Work}
\label{sect:related}
-Dependently typed programming languages have becoming more prominent in recent
+Dependently typed programming languages have become more prominent in recent
years as tools for verifying software correctness, and several experimental
languages are being developed, in particular Agda \cite{norell2007thesis},
Epigram \cite{McBride2004a,Levitation2010} and Trellys \cite{Kimmell2012}.
@@ -39,7 +39,9 @@ \section{Related Work}
combined with unification, making it harder to maintain; secondly, adding new
high level features requires the type checker to support those features
directly. In contrast, elaboration by tactics gives a clean separation between
-the low level and high level languages.
+the low level and high level languages, and results in programs in a core
+type theory which is separately checkable, perhaps even by an independently
+written checker which implements the \TT{} rules directly.
Matita uses a bi-directional refinement algorithm~\cite{Asperti}. This is a
type directed approach, maintaining a set of yet to be solved unification
@@ -141,9 +143,9 @@ \section{Conclusion}
for proof terms, perhaps based on a zipper \cite{Huet1997}. Compilation is made
straightforward by the Epic library \cite{brady2011epic}, with I/O and foreign
functions handled using command-response interaction trees \cite{Hancock2000}.
-Although we have not yet run detailed benchmarks of the performance of compiled
-code, we believe that rich type information and guaranteed termination will
-allow aggressive optimisations~\cite{Brady2003,Brady2005}. We will investigate
+Although I have not yet run detailed benchmarks of the performance of compiled
+code, I believe that rich type information and guaranteed termination will
+allow aggressive optimisations~\cite{Brady2003,Brady2005}. I will investigate
this in future work.
The objective of this implementation of \Idris{} is to provide a platform
@@ -815,7 +815,7 @@ \subsubsection{Example}
in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof
state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.
Note in particular that each tactic which introduces a guess ($\MO{Fill}$
-and $\MO{Solve}$ is closed with a $\MO{Solve}$).
+and $\MO{Attack}$) is closed with a $\MO{Solve}$.
Setting up elaboration in this way, with a proof state captured in a monad,
and a primitive collection of tactics, makes it easy to derive more complex
@@ -944,7 +944,7 @@ \subsection{Elaborating Expressions}
\FFIG{
\AR{
\begin{array}{rll@{\hg}rll}
-\ve ::= & \vc & (\mbox{constant}) &
+\ve, \vt ::= & \vc & (\mbox{constant}) &
\mid & \vx & (\mbox{variable}) \\
\mid & \ilam{\vx}\;\ve & (\mbox{lambda abstraction}) &
\mid & \ve\;\ta & (\mbox{function application}) \\
@@ -1,13 +1,16 @@
Automatically generated by Mendeley 1.6
Any changes to this file will be lost if it is regenerated by Mendeley.
-@inproceedings{Delahaye,
-author = {Delahaye, David},
-booktitle = {Proceedings of Logic for Programming and Automated Reasoning ({LPAR})},
-file = {:Users/edwin/Documents/Mendeley Desktop/Delahaye/A Tactic Language for the System Coq/Delahaye - A Tactic Language for the System Coq - 2000(3).pdf:pdf},
-title = {{A Tactic Language for the System Coq}},
-url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.66.9062},
-year = {2000}
+@article{McBride2007,
+author = {McBride, Conor and Paterson, Ross},
+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/Applicative programming with effects/McBride, Paterson - Applicative programming with effects - 2008.pdf:pdf},
+journal = {Journal of functional programming},
+number = {1},
+pages = {1----13},
+title = {{Applicative programming with effects}},
+url = {http://journals.cambridge.org/abstract_S0956796807006326},
+volume = {18},
+year = {2008}
}
@inproceedings{McBride2006,
author = {McBride, C and Goguen, H and McKinna, J},
@@ -343,14 +346,6 @@ @article{mccann2000packet
volume = {30},
year = {2000}
}
-@article{McBride2007,
-author = {McBride, Conor and Paterson, Ross},
-file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/Applicative programming with effects/McBride, Paterson - Applicative programming with effects - 2007.pdf:pdf},
-journal = {Journal of functional programming},
-title = {{Applicative programming with effects}},
-url = {http://journals.cambridge.org/abstract_S0956796807006326},
-year = {2007}
-}
@misc{Ferreira2012,
annote = {This paper explains how to compile Beluga, a programming language with higher order abstract syntax which is specifically designed to support data structures with binders. In particular, it aims to make it easy to reason about metatheory of programming languages by supporting name generation, alpha conversion and capture avoiding substitution.
@@ -1289,7 +1284,7 @@ @article{Hughes1989
}
@inproceedings{Asperti2011,
author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},
-booktitle = {Automated Deduction --- CADE-23},
+booktitle = {{Automated Deduction --- CADE-23}},
file = {:Users/edwin/Documents/Mendeley Desktop/Asperti et al/The Matita Interactive Theorem Prover/Asperti et al. - The Matita Interactive Theorem Prover - 2011.pdf:pdf},
pages = {64----69},
title = {{The Matita Interactive Theorem Prover}},
@@ -1408,7 +1403,7 @@ @article{landin1966next
}
@inproceedings{Delahaye2000,
author = {Delahaye, D},
-booktitle = {Logic for Programming and Automated Reasoning},
+booktitle = {Logic for Programming and Automated Reasoning ({LPAR})},
file = {:Users/edwin/Documents/Mendeley Desktop/Delahaye/A tactic language for the system Coq/Delahaye - A tactic language for the system Coq - 2000.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Delahaye/A tactic language for the system Coq/Delahaye - A tactic language for the system Coq - 2000(2).pdf:pdf},
pages = {85----95},
publisher = {Springer},
@@ -1426,7 +1421,7 @@ @article{Asperti
author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},
doi = {10.2168/LMCS-},
file = {:Users/edwin/Documents/Mendeley Desktop/Asperti et al/A bi-directional refinement algorithm for the calculus of (co)inductive constructions/Asperti et al. - A bi-directional refinement algorithm for the calculus of (co)inductive constructions - 2012.pdf:pdf},
-journal = {Logical Methods in Computer Science},
+journal = {{Logical Methods in Computer Science}},
keywords = {and phrases,calculus of inductive construc-,interactive theorem prover,refiner,type inference},
pages = {1----49},
title = {{A bi-directional refinement algorithm for the calculus of (co)inductive constructions}},
@@ -1632,6 +1627,14 @@ @article{Thiemann
pages = {1--16},
title = {{Agda Meets Accelerate}}
}
+@inproceedings{Delahaye,
+author = {Delahaye, David},
+booktitle = {Proceedings of Logic for Programming and Automated Reasoning ({LPAR})},
+file = {:Users/edwin/Documents/Mendeley Desktop/Delahaye/A Tactic Language for the System Coq/Delahaye - A Tactic Language for the System Coq - 2000(3).pdf:pdf},
+title = {{A Tactic Language for the System Coq}},
+url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.66.9062},
+year = {2000}
+}
@inproceedings{atkey2009unembedding,
author = {Atkey, R. and Lindley, S. and Yallop, J.},
booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},
@@ -1965,7 +1968,7 @@ @article{Lee2001
file = {:Users/edwin/Documents/Mendeley Desktop/Lee, Jones, Ben-Amram/The size-change principle for program termination/Lee, Jones, Ben-Amram - The size-change principle for program termination - 2001.pdf:pdf},
isbn = {1-58113-336-7},
issn = {03621340},
-journal = {ACM SIGPLAN Notices},
+journal = {{ACM SIGPLAN Notices}},
keywords = {PSPACE-completeness,omega automaton,partial evaluation,program analysis,termination},
month = mar,
number = {3},

0 comments on commit 296588f

Please sign in to comment.