git.iko.soy/Idris-dev
on master help sign in
Revision of impl-paper completed.
commit296588f31d308b5d754b6821522813ba1e7d4148 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 15 Feb 2013, 16:33 (14 years ago) parent091a5df
3 files changed+31−26
compare with master
unifiedsplit
papers/impl-paper/conclusions.tex+7−5 papers/impl-paper/elaboration.tex+2−2 papers/impl-paper/library.bib+22−19
papers/impl-paper/conclusions.tex+7−5
@@ -2,7 +2,7 @@
22
33\label{sect:related}
44
5−Dependently typed programming languages have becoming more prominent in recent
5+Dependently typed programming languages have become more prominent in recent
66years as tools for verifying software correctness, and several experimental
77languages are being developed, in particular Agda \cite{norell2007thesis},
88Epigram \cite{McBride2004a,Levitation2010} and Trellys \cite{Kimmell2012}.
@@ -39,7 +39,9 @@ approach, however: firstly, the type checker is much more complicated when
3939combined with unification, making it harder to maintain; secondly, adding new
4040high level features requires the type checker to support those features
4141directly. In contrast, elaboration by tactics gives a clean separation between
42−the low level and high level languages.
42+the low level and high level languages, and results in programs in a core
43+type theory which is separately checkable, perhaps even by an independently
44+written checker which implements the \TT{} rules directly.
4345
4446Matita uses a bi-directional refinement algorithm~\cite{Asperti}. This is a
4547type directed approach, maintaining a set of yet to be solved unification
@@ -141,9 +143,9 @@ in a proof term, which can be improved by choosing a better representation
141143for proof terms, perhaps based on a zipper \cite{Huet1997}. Compilation is made
142144straightforward by the Epic library \cite{brady2011epic}, with I/O and foreign
143145functions handled using command-response interaction trees \cite{Hancock2000}.
144−Although we have not yet run detailed benchmarks of the performance of compiled
145−code, we believe that rich type information and guaranteed termination will
146−allow aggressive optimisations~\cite{Brady2003,Brady2005}. We will investigate
146+Although I have not yet run detailed benchmarks of the performance of compiled
147+code, I believe that rich type information and guaranteed termination will
148+allow aggressive optimisations~\cite{Brady2003,Brady2005}. I will investigate
147149this in future work.
148150
149151The objective of this implementation of \Idris{} is to provide a platform
papers/impl-paper/elaboration.tex+2−2
@@ -815,7 +815,7 @@ Using this convention, we can build $\FN{id}$'s type and definition as shown
815815in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof
816816state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.
817817Note in particular that each tactic which introduces a guess ($\MO{Fill}$
818−and $\MO{Solve}$ is closed with a $\MO{Solve}$).
818+and $\MO{Attack}$) is closed with a $\MO{Solve}$.
819819
820820Setting up elaboration in this way, with a proof state captured in a monad,
821821and a primitive collection of tactics, makes it easy to derive more complex
@@ -944,7 +944,7 @@ are given explicitly, the application must be expanded.
944944\FFIG{
945945\AR{
946946\begin{array}{rll@{\hg}rll}
947−\ve ::= & \vc & (\mbox{constant}) &
947+\ve, \vt ::= & \vc & (\mbox{constant}) &
948948\mid & \vx & (\mbox{variable}) \\
949949\mid & \ilam{\vx}\;\ve & (\mbox{lambda abstraction}) &
950950\mid & \ve\;\ta & (\mbox{function application}) \\
papers/impl-paper/library.bib+22−19
@@ -1,13 +1,16 @@
11Automatically generated by Mendeley 1.6
22Any changes to this file will be lost if it is regenerated by Mendeley.
33
4−@inproceedings{Delahaye,
5−author = {Delahaye, David},
6−booktitle = {Proceedings of Logic for Programming and Automated Reasoning ({LPAR})},
7−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},
8−title = {{A Tactic Language for the System Coq}},
9−url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.66.9062},
10−year = {2000}
4+@article{McBride2007,
5+author = {McBride, Conor and Paterson, Ross},
6+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/Applicative programming with effects/McBride, Paterson - Applicative programming with effects - 2008.pdf:pdf},
7+journal = {Journal of functional programming},
8+number = {1},
9+pages = {1----13},
10+title = {{Applicative programming with effects}},
11+url = {http://journals.cambridge.org/abstract_S0956796807006326},
12+volume = {18},
13+year = {2008}
1114}
1215@inproceedings{McBride2006,
1316author = {McBride, C and Goguen, H and McKinna, J},
@@ -343,14 +346,6 @@ url = {http://dl.acm.org/citation.cfm?id=347563},
343346volume = {30},
344347year = {2000}
345348}
346−@article{McBride2007,
347−author = {McBride, Conor and Paterson, Ross},
348−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/Applicative programming with effects/McBride, Paterson - Applicative programming with effects - 2007.pdf:pdf},
349−journal = {Journal of functional programming},
350−title = {{Applicative programming with effects}},
351−url = {http://journals.cambridge.org/abstract_S0956796807006326},
352−year = {2007}
353−}
354349@misc{Ferreira2012,
355350annote = {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.
356351
@@ -1289,7 +1284,7 @@ year = {1989}
12891284}
12901285@inproceedings{Asperti2011,
12911286author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},
1292−booktitle = {Automated Deduction --- CADE-23},
1287+booktitle = {{Automated Deduction --- CADE-23}},
12931288file = {:Users/edwin/Documents/Mendeley Desktop/Asperti et al/The Matita Interactive Theorem Prover/Asperti et al. - The Matita Interactive Theorem Prover - 2011.pdf:pdf},
12941289pages = {64----69},
12951290title = {{The Matita Interactive Theorem Prover}},
@@ -1408,7 +1403,7 @@ year = {1966}
14081403}
14091404@inproceedings{Delahaye2000,
14101405author = {Delahaye, D},
1411−booktitle = {Logic for Programming and Automated Reasoning},
1406+booktitle = {Logic for Programming and Automated Reasoning ({LPAR})},
14121407file = {: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},
14131408pages = {85----95},
14141409publisher = {Springer},
@@ -1426,7 +1421,7 @@ title = {{HTTP: The Definitive Guide Chapter 3}}
14261421author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},
14271422doi = {10.2168/LMCS-},
14281423file = {: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},
1429−journal = {Logical Methods in Computer Science},
1424+journal = {{Logical Methods in Computer Science}},
14301425keywords = {and phrases,calculus of inductive construc-,interactive theorem prover,refiner,type inference},
14311426pages = {1----49},
14321427title = {{A bi-directional refinement algorithm for the calculus of (co)inductive constructions}},
@@ -1632,6 +1627,14 @@ keywords = {data parallelism,programming with dependent types},
16321627pages = {1--16},
16331628title = {{Agda Meets Accelerate}}
16341629}
1630+@inproceedings{Delahaye,
1631+author = {Delahaye, David},
1632+booktitle = {Proceedings of Logic for Programming and Automated Reasoning ({LPAR})},
1633+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},
1634+title = {{A Tactic Language for the System Coq}},
1635+url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.66.9062},
1636+year = {2000}
1637+}
16351638@inproceedings{atkey2009unembedding,
16361639author = {Atkey, R. and Lindley, S. and Yallop, J.},
16371640booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},
@@ -1965,7 +1968,7 @@ doi = {10.1145/373243.360210},
19651968file = {: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},
19661969isbn = {1-58113-336-7},
19671970issn = {03621340},
1968−journal = {ACM SIGPLAN Notices},
1971+journal = {{ACM SIGPLAN Notices}},
19691972keywords = {PSPACE-completeness,omega automaton,partial evaluation,program analysis,termination},
19701973month = mar,
19711974number = {3},