1
0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 19:18:25 +00:00

References for OCaml, Scheme, and proper tail recursion.

This commit is contained in:
2020-09-23 20:32:55 +01:00
parent 471a17dd5d
commit e623e1ecd0
2 changed files with 41 additions and 2 deletions

View File

@@ -769,6 +769,28 @@
address = {Cambridge, MA, USA}, address = {Cambridge, MA, USA},
} }
# OCaml
@book{LeroyDFGRV20,
author = {Xavier Leroy and Damien Doligez and Alain Frisch and Jacques Garrigue and Didier Rémy and Jérôme Vouillon},
title = {The {OCaml} System Release 4.11: Documentation and user's manual},
year = 2020,
month = aug,
publisher = {Institut National de Recherche en Informatique et en Automatique}
}
# Scheme R6RS
@book{SperberDFSFM10,
author = {Michael Sperber and
R. Kent Dybvig and
Matthew Flatt and
Anton van Straaten and
Robert Bruce Findler and
Jacob Matthews},
title = {Revised6 Report on the Algorithmic Language Scheme},
publisher = {Cambridge University Press},
year = {2010}
}
# Timeless classics # Timeless classics
@article{Plotkin04a, @article{Plotkin04a,
author = {Gordon D. Plotkin}, author = {Gordon D. Plotkin},
@@ -813,7 +835,7 @@
year = {1994} year = {1994}
} }
% Control operators # Control operators
@article{Landin65, @article{Landin65,
author = {Peter J. Landin}, author = {Peter J. Landin},
title = {Correspondence between {ALGOL} 60 and Church's Lambda-notation: part title = {Correspondence between {ALGOL} 60 and Church's Lambda-notation: part
@@ -846,7 +868,7 @@
year = {1998} year = {1998}
} }
% System F # System F
@phdthesis{Girard72, @phdthesis{Girard72,
author = {J. Y. Girard}, author = {J. Y. Girard},
school = {Universit{\'e} Paris 7}, school = {Universit{\'e} Paris 7},
@@ -875,3 +897,12 @@
year = {1989} year = {1989}
} }
# Tail calls
@inproceedings{Clinger98,
author = {William D. Clinger},
title = {Proper Tail Recursion and Space Efficiency},
booktitle = {{PLDI}},
pages = {174--185},
publisher = {{ACM}},
year = {1998}
}

View File

@@ -881,6 +881,14 @@ bindings, pair deconstructing, and case splitting. In each of those
cases we subtract the relevant binder(s) from the set of free cases we subtract the relevant binder(s) from the set of free
variables. variables.
\paragraph{Proper tail-recursion}
Many industrial-strength functional programming languages such as
SML~\cite{MilnerTHM97}, OCaml~\cite{LeroyDFGRV20},
Scheme~\cite{SperberDFSFM10} rely heavily on being properly
tail-recursive\dots
\dhil{TODO define properly tail-recursive}
\subsection{Typing rules} \subsection{Typing rules}
\label{sec:base-language-type-rules} \label{sec:base-language-type-rules}
% %