Permalink
Browse files

Started paper

  • Loading branch information...
1 parent 6b70dd1 commit 819e50edcbe93e0626dec1502ef9545f0869f2a7 Edwin Brady committed Dec 17, 2010
View
@@ -0,0 +1,36 @@
+PAPER = epic
+
+all: ${PAPER}.pdf
+
+TEXFILES = ${PAPER}.tex intro.tex language.tex example.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:
View
@@ -0,0 +1,29 @@
+% $id$
+% KH: created comments style file to allow alternative versions of a document.
+
+% \newcommand{\red}[1]{#1}
+
+\usepackage{color}
+\definecolor{BrickRed}{cmyk}{0, .89, .5, 0}
+\newcommand{\red}{\color{BrickRed}}
+
+\newcommand{\eucommentary}[1]{\(\spadesuit\){\red{\textbf{EC Commentary}: \emph{#1}}\(\spadesuit\)}}
+\newcommand{\euevaluation}[2]{\(\spadesuit\){\red{\textbf{Evaluation Criteria ({#1})}: \emph{#2}}\(\spadesuit\)}}
+
+\newcommand{\comment}[2]{\(\spadesuit\){\bf #1: }{\rm \sf #2}\(\spadesuit\)}
+\newcommand{\draftpage}{\newpage}
+
+\newcommand{\FIXME}[1]{[\textbf{FIXME}: #1]}
+
+%\newcommand{\FIXME}[1]{\wibble}
+\newcommand{\nocomments}{
+\renewcommand{\eucommentary}[1]{}
+\renewcommand{\euevaluation}[2]{}
+\renewcommand{\comment}[2]{}
+\renewcommand{\draftpage}{}
+\renewcommand{\FIXME}[1]{}
+}
+
+\DeclareOption{final}{\nocomments}
+\DeclareOption{draft}{}
+\ProcessOptions*
@@ -0,0 +1,5 @@
+\section{Related Work}
+
+
+\section{Conclusion}
+
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 819e50e

Please sign in to comment.