Skip to content
Permalink
Browse files

Add references for compilation paper etc.

  • Loading branch information...
kwxm committed Jun 16, 2019
1 parent b036f43 commit f7d955fa6ac82b8cf6fca5b9473582d3069e1bff
@@ -20,6 +20,7 @@ all: pdf
pdf: ${PDF}

${DOC}.pdf: ${SRC}
-rm -f ${DOC}.bbl ${DOC}.aux
${LATEX} ${DOC}
${BIBTEX} ${DOC}
${LATEX} ${DOC} # to make sure the (cross)references are correct
@@ -21,6 +21,16 @@ @book{Pierce:ATTAPL
homepage = {http://www.cis.upenn.edu/~bcpierce/attapl}
}

@incollection{Pitts:typed-operational-reasoning,
author={Pitts, A.M.},
title={Typed Operational Reasoning},
chapter=7,
editor = {Benjamin C. Pierce},
booktitle = {Advanced Topics in Types and Programming Languages},
publisher = {MIT Press},
year = 2005
}

@book{Harper:PFPL,
author = {Harper, Robert},
title = {Practical Foundations for Programming Languages},
@@ -54,8 +64,6 @@ @article{Friedman-Lazy-Krivine
issn = {1388-3690},
pages = {271--293},
numpages = {23},
url = {http://dx.doi.org/10.1007/s10990-007-9014-0},
doi = {10.1007/s10990-007-9014-0},
acmid = {1325155},
publisher = {Kluwer Academic Publishers},
address = {Hingham, MA, USA},
@@ -75,8 +83,6 @@ @article{Felleisen-Hieb
issn = {0304-3975},
pages = {235--271},
numpages = {37},
url = {http://dx.doi.org/10.1016/0304-3975(92)90014-7},
doi = {10.1016/0304-3975(92)90014-7},
acmid = {136297},
publisher = {Elsevier Science Publishers Ltd.},
address = {Essex, UK},
@@ -102,8 +108,7 @@ @inproceedings{reynolds-type-structure
volume = {19},
series = {Lecture Notes in Computer Science},
month = apr,
publisher = {Springer},
url = {http://www.springerlink.com/content/p5801737k78207p7/}
publisher = {Springer}
}

@unpublished{Scott-encoding,
@@ -120,13 +125,10 @@ @inproceedings{Koopman:2014
booktitle = {Proceedings of the 26Nd 2014 International Symposium on Implementation and Application of Functional Languages},
series = {IFL '14},
year = {2014},
isbn = {978-1-4503-3284-2},
location = {Boston, MA, USA},
pages = {4:1--4:12},
articleno = {4},
numpages = {12},
url = {http://doi.acm.org/10.1145/2746325.2746330},
doi = {10.1145/2746325.2746330},
acmid = {2746330},
publisher = {ACM},
address = {New York, NY, USA},
@@ -146,8 +148,6 @@ @article{Ahmed:2017
pages = {39:1--39:28},
articleno = {39},
numpages = {28},
url = {http://doi.acm.org/10.1145/3110283},
doi = {10.1145/3110283},
acmid = {3110283},
publisher = {ACM},
address = {New York, NY, USA},
@@ -181,12 +181,9 @@ @inproceedings{Yakushev2009
booktitle = {Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming},
series = {ICFP '09},
year = {2009},
isbn = {978-1-60558-332-7},
location = {Edinburgh, Scotland},
pages = {233--244},
numpages = {12},
url = {http://doi.acm.org/10.1145/1596550.1596585},
doi = {10.1145/1596550.1596585},
acmid = {1596585},
publisher = {ACM},
address = {New York, NY, USA},
@@ -198,7 +195,6 @@ @book{Princeton-bitcoin-book
author = {Narayanan, Arvind and Bonneau, Joseph and Felten, Edward and Miller, Andrew and Goldfeder, Steven},
title = {Bitcoin and Cryptocurrency Technologies: A Comprehensive Introduction},
year = {2016},
isbn = {0691171696, 9780691171692},
publisher = {Princeton University Press},
address = {Princeton, NJ, USA},
}
@@ -233,3 +229,18 @@ @article{Zahnentferner18-UTxO
}


@inproceedings{compiling-to-fomega-2019,
author = {Roman Kireev and Chad Nester and Michael Peyton Jones and Philip Wadler and Vasilis Gkoumas and Kenneth {MacKenzie}},
title = {Unraveling recursion: compiling an {IR} with recursion to {System~$F$}},
booktitle = {Proceedings of MPC 2019},
year={2019},
note = {To appear}
}

@inproceedin{system-F-in-Agda,
author = {James Chapman and Roman Kireev and Chad Nester and Philip Wadler},
title = {{System~$F$} in {Agda}, for fun and profit},
booktitle = {Proceedings of MPC 2019},
year={2019},
note = {To appear}
}
@@ -448,16 +448,18 @@ \subsubsection{Recursive types}
Plutus Core: \texttt{ifix A B} is a type such that \texttt{ifix A B
$\cong$ A (ifix A) B} where \texttt{A} is a \textit{pattern
functor}~\citep[2.4]{backhouseetal98} and \texttt{B} is an
index. Pattern functors that \texttt{ifix} receives bind two variables:
one for building recursive occurrences and the other to act as an
index. Indices can be used in order to get parameterised data types,
but also in order to control the shape of the data type: depending on
an index, recursive occurrences can be instantiated differently. This
allows us to encode a wide variety of data types, including non-regular and
mutually recursive data types\blue{\footnote{\blue{We could do with more detail (or perhaps an example) here, since
it'll be much more difficult for the reader to work out what's going
on than with standard \texttt{fix}. With luck we'll soon have a publication
to refer to.}}}.
index. Pattern functors that \texttt{ifix} receives bind two
variables: one for building recursive occurrences and the other to act
as an index. Indices can be used in order to get parameterised data
types, but also in order to control the shape of the data type:
depending on an index, recursive occurrences can be instantiated
differently. This allows us to encode a wide variety of data types,
including non-regular and mutually recursive data types.%
\blue{\footnote{\blue{We could do with more detail (or perhaps an
example) here, since it'll be much more difficult for the reader
to work out what's going on than with standard \texttt{fix}. Is
the compilation paper sufficient?}}}
See~\cite{compiling-to-fomega-2019} for more details.

Note that we have an \textit{isomporhism} of types here rather than
equality: fixpoint types are
@@ -497,8 +499,10 @@ \subsubsection{The value restriction}
number of difficulties. For example, Standard ML's value restriction
is required to avoid a number of problems when (implicit) type
abstractions include non-values; other issues are explored
in~\citep[2.4]{Ahmed:2017}. Plutus Core's restriction to values avoids
these problems and is not very onerous in practice.
in~\citep[2.4]{Ahmed:2017}
and~\citep[7.4.1]{Pitts:typed-operational-reasoning}. Plutus Core's
restriction to values avoids these problems and is not very onerous in
practice.

\section{Type Correctness}

0 comments on commit f7d955f

Please sign in to comment.
You can’t perform that action at this time.