pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Tiny revisions to LambdaCalculusAndTypeSoundness

Browse source
This commit is contained in:
Adam Chlipala 2017-04-02 19:18:34 -04:00
parent 119996a90c
commit e204041ff8
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
LambdaCalculusAndTypeSoundness_template.v
View file

@ -591,7 +591,7 @@ Module Stlc.
Proof.
Admitted.
Theorem safety_snazzy : forall e t, hasty $0 e t
Theorem safety : forall e t, hasty $0 e t
-> invariantFor (trsys_of e) unstuck.
Proof.
simplify.

2
frap_book.tex
View file

@ -2553,7 +2553,7 @@ We write $\smallstepcls{s}{\ell}{s'}$ to indicate that $s$ steps to $s'$ via zer
\chapter{Lambda Calculus and Simple Type Safety}
We'll now take a break from the imperative language we've been studying for the last two chapters, instead looking at a classic sort of small language that distills the essence of \emph{functional} programming\index{functional programming}.
We'll now take a break from the imperative language we've been studying for the last three chapters, instead looking at a classic sort of small language that distills the essence of \emph{functional} programming\index{functional programming}.
That's the language paradigm that we've been using throughout this book, as we coded executable versions of algorithms.
Its distinctive characteristics are first, a computation style based on simplifying terms instead of running step-by-step instructions that modify state; and second, use of functions as first-class values.
Functional programming went mainstream in the early 21st century, influencing widely adopted languages from JavaScript\index{JavaScript}, where first-class functions are routinely used as callbacks in asynchronous event processing; to Scala\index{Scala}, a hybrid language that melds functional-programming ideas with object-oriented programming for the Java platform; to Haskell\index{Haskell}, a purely functional language that has become popular with programming hobbyists and is seeing increasing adoption in industry.