From e623e1ecd01637efeb1c1aa1bbb4d133604c0c70 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 23 Sep 2020 20:32:55 +0100 Subject: [PATCH] References for OCaml, Scheme, and proper tail recursion. --- thesis.bib | 35 +++++++++++++++++++++++++++++++++-- thesis.tex | 8 ++++++++ 2 files changed, 41 insertions(+), 2 deletions(-) diff --git a/thesis.bib b/thesis.bib index c5cc28f..9aca4ab 100644 --- a/thesis.bib +++ b/thesis.bib @@ -769,6 +769,28 @@ 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 @article{Plotkin04a, author = {Gordon D. Plotkin}, @@ -813,7 +835,7 @@ year = {1994} } -% Control operators +# Control operators @article{Landin65, author = {Peter J. Landin}, title = {Correspondence between {ALGOL} 60 and Church's Lambda-notation: part @@ -846,7 +868,7 @@ year = {1998} } -% System F +# System F @phdthesis{Girard72, author = {J. Y. Girard}, school = {Universit{\'e} Paris 7}, @@ -875,3 +897,12 @@ 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} +} \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index d6b38c5..745189b 100644 --- a/thesis.tex +++ b/thesis.tex @@ -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 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} \label{sec:base-language-type-rules} %