Permalink
Browse files

Added TFP abstract

  • Loading branch information...
Edwin Brady
Edwin Brady committed Apr 22, 2011
1 parent 704a735 commit 15e4778658a90f586ab9d191429bd272a8778e19
View
@@ -0,0 +1,36 @@
+PAPER = epic
+
+all: ${PAPER}.pdf
+
+TEXFILES = ${PAPER}.tex intro.tex language.tex example.tex \
+ implementation.tex performance.tex conclusions.tex
+
+DIAGS =
+
+SOURCES = ${TEXFILES} ${DIAGS} macros.ltx literature.bib
+
+DITAA = java -jar ~/Downloads/ditaa.jar
+
+${PAPER}.pdf: ${SOURCES}
+# dvipdf ${PAPER}.dvi
+ pdflatex ${PAPER}
+ -bibtex ${PAPER}
+ -pdflatex ${PAPER}
+ -pdflatex ${PAPER}
+
+${PAPER}.ps: ${PAPER}.dvi
+ dvips -o ${PAPER}.ps ${PAPER}
+
+${PAPER}.dvi: $(SOURCES)
+ -latex ${PAPER}
+ -bibtex ${PAPER}
+ -latex ${PAPER}
+ -latex ${PAPER}
+
+progress: .PHONY
+ wc -w ${TEXFILES}
+
+%.png : %.diag
+ $(DITAA) -o -E $<
+
+.PHONY:
@@ -0,0 +1,34 @@
+\section{Related Work}
+
+%% GHC's run-time system~\cite{stg, evalpush}, ABC
+%% machine~\cite{abc-machine} and why we don't just use one of them
+%% (no useful interface, imposes constraints on the type system).
+%% Some influence from GRIN~\cite{grin-project}.
+
+Epic is currently used by Agda and Idris~\cite{plpv11}, as well as the
+development version of Epigram~\cite{levitation}. Initial
+benchmarking~\cite{scrap-engine} shows that the code generated by Epic
+can be competitive with Java and is not significantly worse than C.
+Epic uses techniques from other functional language back
+ends~\cite{evalpush,stg,abc-machine} but deliberately exposes its core
+language as an API to make it as reusable as possible. Although there
+is likely to always be a trade off between reusability and efficiency,
+exposing the API will make it easier for other language researchers to
+build a new compiler quickly. The Lazy Virtual Machine~\cite{lvm} has
+similar goals but it designed as a lower level target language, rather
+than a high level API.
+
+%C--~\cite{c--} and LLVM~\cite{llvm}
+%as possible code generation strategies. Supercompilation for
+%optimisations~\cite{mitchell-super}.
+
+\section{Conclusion}
+
+Epic provides a simple path for language researchers to convert
+experimental languages (e.g. experimenting with new type systems or
+domain specific language design) into larger scale, usable tools, by
+providing an API for generating a compiler, dealing with
+well-understood but difficult to implement problems such as lambda
+lifting, code generation, interfacing with foreign functions and
+garbage collection.
+
View
@@ -0,0 +1,151 @@
+@phdthesis{ brady-thesis,
+ author = {Edwin Brady},
+ title = {Practical Implementation of a Dependently Typed Functional Programming Language},
+ year = 2005,
+ school = {University of Durham}
+}
+
+@article{view-left,
+ journal = {Journal of Functional Programming},
+ number = {1},
+ volume = {14},
+ title = {The View From The Left},
+ year = {2004},
+ author = {Conor McBride and James McKinna},
+ pages = {69--111}
+}
+
+@misc{epigram-afp,
+ author = {Conor McBride},
+ title = {Epigram: Practical Programming with Dependent Types},
+ year = {2004},
+ howpublished = {Lecture Notes, International Summer School on Advanced Functional Programming}
+}
+
+@misc{coq-manual,
+ howpublished = {\verb+http://coq.inria.fr/+},
+ title = {The {Coq} Proof Assistant --- Reference Manual},
+ year = {2004},
+ author = {{Coq Development Team}}
+}
+
+@inproceedings{extraction-coq,
+ title = {A New Extraction for {Coq}},
+ year = {2002},
+ booktitle = {Types for proofs and programs},
+ editor = {Herman Geuvers and Freek Wiedijk},
+ publisher = {Springer},
+ author = {Pierre Letouzey},
+ series = {LNCS}
+}
+
+@techreport{lego-manual,
+ title = {\textsc{Lego} Proof Development System: User's Manual},
+ year = {1992},
+ institution = {Department of Computer Science, University of Edinburgh},
+ author = {Zhaohui Luo and Robert Pollack}
+}
+
+@book{luo94,
+ title = {Computation and Reasoning -- A Type Theory for Computer Science},
+ year = {1994},
+ publisher = {OUP},
+ author = {Zhaohui Luo},
+ series = {International Series of Monographs on Computer Science}
+}
+
+@phdthesis{goguen-thesis,
+ school = {University of Edinburgh},
+ title = {A Typed Operational Semantics for Type Theory},
+ year = {1994},
+ author = {Healfdene Goguen}
+}
+
+@phdthesis{mcbride-thesis,
+ month = {May},
+ school = {University of Edinburgh},
+ title = {Dependently Typed Functional Programs and their proofs},
+ year = {2000},
+ author = {Conor McBride}
+}
+
+@misc{mckinnabrady-phase,
+ title = {Phase Distinctions in the Compilation of {Epigram}},
+ year = 2005,
+ author = {James McKinna and Edwin Brady},
+ note = {Draft}
+}
+
+@article{pugh-omega,
+ title = "The {Omega} {Test}: a fast and practical integer programming algorithm for dependence analysis",
+ author = "William Pugh",
+ journal = "Communication of the ACM",
+ year = 1992,
+ pages = {102--114}
+}
+
+@Article{RegionTypes,
+ refkey = "C1753",
+ title = "Region-Based Memory Management",
+ author = "M. Tofte and J.-P. Talpin",
+ pages = "109--176",
+ journal = "Information and Computation",
+ month = "1~" # feb,
+ year = "1997",
+ volume = "132",
+ number = "2"
+}
+
+@phdthesis{ pedro-thesis,
+ author = {Pedro Vasconcelos},
+ title = {Space Cost Modelling for Concurrent Resource Sensitive Systems},
+ year = 2006,
+ school = {University of St Andrews}
+}
+
+@book{curry-feys,
+ title = {Combinatory Logic, volume 1},
+ year = {1958},
+ publisher = {North Holland},
+ author = {Haskell B. Curry and Robert Feys}
+}
+@inproceedings{howard,
+ title = {The formulae-as-types notion of construction},
+ year = {1980},
+ booktitle = {To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism},
+ editor = {Jonathan P. Seldin and J. Roger Hindley},
+ publisher = {Academic Press},
+ author = {William A. Howard},
+ note = {A reprint of an unpublished manuscript from 1969}
+}
+
+@misc{ydtm,
+ author = {Thorsten Altenkirch and Conor McBride and James McKinna},
+ title = {Why Dependent Types Matter},
+ note = {Submitted for publication},
+ year = 2005}
+
+@inproceedings{regular-types,
+ author = { Peter Morris and Conor McBride and Thorsten Altenkirch},
+ title = {Exploring The Regular Tree Types},
+ year = 2005,
+ booktitle = {Types for Proofs and Programs 2004}
+}
+
+@inproceedings{xi_arraybounds,
+author = "Hongwei Xi and Frank Pfenning",
+title = {Eliminating Array Bound Checking through Dependent Types},
+booktitle = "Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation",
+year = 1998,
+month = "June",
+address = "Montreal",
+pages = "249--257",
+}
+
+@misc{interp-cayenne,
+ url = {\verb+http://www.cs.chalmers.se/~augustss/cayenne/+},
+ title = {An exercise in dependent types: A well-typed interpreter},
+ year = {1999},
+ author = {Lennart Augustsson and Magnus Carlsson}
+}
+
Oops, something went wrong.

0 comments on commit 15e4778

Please sign in to comment.