296588f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Revision of impl-paper completed.

296588fEdwin Brady14 years ago

papers/impl-paper/conclusions.tex+7−5

compare with master

unifiedsplit

@@ -2,7 +2,7 @@

3\label{sect:related}

5−Dependently typed programming languages have becoming more prominent in recent

5+Dependently typed programming languages have become more prominent in recent

6years as tools for verifying software correctness, and several experimental

7languages are being developed, in particular Agda \cite{norell2007thesis},

8Epigram \cite{McBride2004a,Levitation2010} and Trellys \cite{Kimmell2012}.

@@ -39,7 +39,9 @@ approach, however: firstly, the type checker is much more complicated when

39combined with unification, making it harder to maintain; secondly, adding new

40high level features requires the type checker to support those features

41directly. 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.

44Matita uses a bi-directional refinement algorithm~\cite{Asperti}. This is a

46Matita uses a bi-directional refinement algorithm~\cite{Asperti}. This is a

45type directed approach, maintaining a set of yet to be solved unification

47type 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

141for proof terms, perhaps based on a zipper \cite{Huet1997}. Compilation is made

143for proof terms, perhaps based on a zipper \cite{Huet1997}. Compilation is made

142straightforward by the Epic library \cite{brady2011epic}, with I/O and foreign

144straightforward by the Epic library \cite{brady2011epic}, with I/O and foreign

143functions handled using command-response interaction trees \cite{Hancock2000}.

145functions handled using command-response interaction trees \cite{Hancock2000}.

144−Although we have not yet run detailed benchmarks of the performance of compiled

146+Although I have not yet run detailed benchmarks of the performance of compiled

145−code, we believe that rich type information and guaranteed termination will

147+code, I believe that rich type information and guaranteed termination will

146−allow aggressive optimisations~\cite{Brady2003,Brady2005}. We will investigate

148+allow aggressive optimisations~\cite{Brady2003,Brady2005}. I will investigate

147this in future work.

149this in future work.

148

150

149The objective of this implementation of \Idris{} is to provide a platform

151The 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

815in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof

816state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.

817Note 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}$.

819

820Setting up elaboration in this way, with a proof state captured in a monad,

821and a primitive collection of tactics, makes it easy to derive more complex

@@ -944,7 +944,7 @@ are given explicitly, the application must be expanded.

944\FFIG{

945\AR{

946\begin{array}{rll@{\hg}rll}

947−\ve ::= & \vc & (\mbox{constant}) &

947+\ve, \vt ::= & \vc & (\mbox{constant}) &

948\mid & \vx & (\mbox{variable}) \\

949\mid & \ilam{\vx}\;\ve & (\mbox{lambda abstraction}) &

950\mid & \ve\;\ta & (\mbox{function application}) \\

papers/impl-paper/library.bib+22−19

@@ -1,13 +1,16 @@

1Automatically generated by Mendeley 1.6

2Any changes to this file will be lost if it is regenerated by Mendeley.

4−@inproceedings{Delahaye,

4+@article{McBride2007,

5−author = {Delahaye, David},

5+author = {McBride, Conor and Paterson, Ross},

6−booktitle = {Proceedings of Logic for Programming and Automated Reasoning ({LPAR})},

6+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/Applicative programming with effects/McBride, Paterson - Applicative programming with effects - 2008.pdf:pdf},

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},

7+journal = {Journal of functional programming},

8−title = {{A Tactic Language for the System Coq}},

8+number = {1},

9−url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.66.9062},

9+pages = {1----13},

10+title = {{Applicative programming with effects}},

11+url = {http://journals.cambridge.org/abstract_S0956796807006326},

12+volume = {18},

10−year = {2000}

13+year = {2008}

11}

14}

12@inproceedings{McBride2006,

15@inproceedings{McBride2006,

13author = {McBride, C and Goguen, H and McKinna, J},

16author = {McBride, C and Goguen, H and McKinna, J},

@@ -343,14 +346,6 @@ url = {http://dl.acm.org/citation.cfm?id=347563},

343volume = {30},

346volume = {30},

344year = {2000}

347year = {2000}

345}

348}

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−}

354@misc{Ferreira2012,

349@misc{Ferreira2012,

355annote = {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.

350annote = {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.

356

351

@@ -1289,7 +1284,7 @@ year = {1989}

1289}

1284}

1290@inproceedings{Asperti2011,

1285@inproceedings{Asperti2011,

1291author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},

1286author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},

1292−booktitle = {Automated Deduction --- CADE-23},

1287+booktitle = {{Automated Deduction --- CADE-23}},

1293file = {:Users/edwin/Documents/Mendeley Desktop/Asperti et al/The Matita Interactive Theorem Prover/Asperti et al. - The Matita Interactive Theorem Prover - 2011.pdf:pdf},

1288file = {:Users/edwin/Documents/Mendeley Desktop/Asperti et al/The Matita Interactive Theorem Prover/Asperti et al. - The Matita Interactive Theorem Prover - 2011.pdf:pdf},

1294pages = {64----69},

1289pages = {64----69},

1295title = {{The Matita Interactive Theorem Prover}},

1290title = {{The Matita Interactive Theorem Prover}},

@@ -1408,7 +1403,7 @@ year = {1966}

1408}

1403}

1409@inproceedings{Delahaye2000,

1404@inproceedings{Delahaye2000,

1410author = {Delahaye, D},

1405author = {Delahaye, D},

1411−booktitle = {Logic for Programming and Automated Reasoning},

1406+booktitle = {Logic for Programming and Automated Reasoning ({LPAR})},

1412file = {: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},

1407file = {: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},

1413pages = {85----95},

1408pages = {85----95},

1414publisher = {Springer},

1409publisher = {Springer},

@@ -1426,7 +1421,7 @@ title = {{HTTP: The Definitive Guide Chapter 3}}

1426author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},

1421author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},

1427doi = {10.2168/LMCS-},

1422doi = {10.2168/LMCS-},

1428file = {: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},

1423file = {: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}},

1430keywords = {and phrases,calculus of inductive construc-,interactive theorem prover,refiner,type inference},

1425keywords = {and phrases,calculus of inductive construc-,interactive theorem prover,refiner,type inference},

1431pages = {1----49},

1426pages = {1----49},

1432title = {{A bi-directional refinement algorithm for the calculus of (co)inductive constructions}},

1427title = {{A bi-directional refinement algorithm for the calculus of (co)inductive constructions}},

@@ -1632,6 +1627,14 @@ keywords = {data parallelism,programming with dependent types},

1632pages = {1--16},

1627pages = {1--16},

1633title = {{Agda Meets Accelerate}}

1628title = {{Agda Meets Accelerate}}

1634}

1629}

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+}

1635@inproceedings{atkey2009unembedding,

1638@inproceedings{atkey2009unembedding,

1636author = {Atkey, R. and Lindley, S. and Yallop, J.},

1639author = {Atkey, R. and Lindley, S. and Yallop, J.},

1637booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},

1640booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},

@@ -1965,7 +1968,7 @@ doi = {10.1145/373243.360210},

1965file = {: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},

1968file = {: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},

1966isbn = {1-58113-336-7},

1969isbn = {1-58113-336-7},

1967issn = {03621340},

1970issn = {03621340},

1968−journal = {ACM SIGPLAN Notices},

1971+journal = {{ACM SIGPLAN Notices}},

1969keywords = {PSPACE-completeness,omega automaton,partial evaluation,program analysis,termination},

1972keywords = {PSPACE-completeness,omega automaton,partial evaluation,program analysis,termination},

1970month = mar,

1973month = mar,

1971number = {3},

1974number = {3},