michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

added submitted version to repository

Browse source
This commit is contained in:
wadler 2019-07-21 14:31:40 +01:00
parent ea343fae2e
commit 5e1dc3ef7c
2 changed files with 1088 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1080
papers/scp/PLFA-submitted.tex Executable file
View file

File diff suppressed because it is too large Load diff

17
papers/scp/PLFA.tex
View file

@ -50,7 +50,7 @@
that constructive proofs of preservation and progress give immediate
rise to a prototype evaluator. This fact is obvious in retrospect
but it is not exploited in SF (which instead provides a separate
normalise tactic) nor can I find it in the literature. Third, that
normalise tactic) nor can we find it in the literature. Third, that
using extrinsically-typed terms is far less
perspicuous than using intrinsically-typed terms. SF uses the former
presentation, while PLFA presents both; the former uses about 1.6 as
@ -726,10 +726,10 @@ Some researchers are clearly familiar with the connection between
progress and preservation and animation. In private correspondence,
Bob Harper referred to it as the \emph{pas de deux}, a dance between
progress, which takes well-typing to a step, and preservation, which
takes a step back to well-typing. Nonetheless, neither the technique
takes a step back to well-typing---but neither the technique
nor the appealing terminology appears in \citet{Harper-2016}. The
appeal to the Agda mailing list bore late fruit: Oleg Kiselyov
directed me to unpublished remarks on his web page where he uses the
directed us to unpublished remarks on his web page where he uses the
name \texttt{eval} for a proof of progress and notes ``the very proof
of type soundness can be used to evaluate sample expressions''
\citep{Kiselyov-2009}. Nonetheless, as of this writing, we still have
@ -740,7 +740,7 @@ There are places in the literature where one might expect a remark on
the relation between progress and preservation and animation---but no
such remark appears. In the PoplMark Challenge
\citep{Aydemir-et-al-2005}, Challenge~2A is to prove progress and
preservation for System F$_{<:}$, while Challenge~3 is to prove
preservation for System~F$_{<:}$, while Challenge~3 is to prove
animation for the same system. Nowhere do the authors indicate that in
an intuitionistic logic these are essentially the same problem.
\cite{Owens-et-al-2016}, when discussing extraction of animators for
@ -751,9 +751,6 @@ connection becomes more widely known.
\section{Intrinsic typing is golden}
\begin{figure}[p]
@ -861,14 +858,16 @@ teaching from PLFA. To date, he has taught three courses from PLFA.
assistance from Wen and Chad Nester); twenty 2-hour slots,
comprising one hour of lecture followed by one hour of lab. Ten
students completed the course, fourth-year undergraduates and
masters. The course covered Parts~I and~II of PLFA.
masters. The course covered Parts~I and~II of PLFA, up through
chapter Untyped.
\item
Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio),
March--July 2019, hosted by Roberto Ieuramalischy; ten 3-hour
slots, comprising two hours of lecture followed by one hour of lab.
Ten students completed the course, mostly doctoral students. The
course covered Parts~I and~II of PLFA, save students read chapter
course covered Parts~I and~II of PLFA, up through chapter Untyped,
save students read chapter
Lists on their own, and chapter Bisimilarity was skipped.
\item