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

Wrote announcement for Part 3

Browse source
This commit is contained in:
Wen Kokke 2020-07-13 23:37:01 +01:00
parent 11d8dff177
commit c56db8000d
3 changed files with 23 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
_posts/2019-07-12-changes-to-plfa.md
View file

@ -1,6 +1,6 @@
---
layout : post
title : "Changes to PLFA – Migration to Agda 2.6"
title : "Migration to Agda 2.6"
---
Today, we made several major changes to the PLFA infrastructure!

13
_posts/2020-07-13-denotational-semantics.md Normal file
View file

@ -0,0 +1,13 @@
---
layout : post
title : "Introducing Part 3: Denotational Semantics"
---
We’re pleased to announce an entirely new part of the book, contributed by Jeremy G. Siek! You may have noticed his name appearing on the list of authors some months ago, or the chapters that make up Part 3 slowly making their appearance. Well, that’s all Jeremy’s work!
Part 3 introduces denotational semantics, presenting the denotational semantics of the untyped lambda calculus. Our development is unusual in that emphasizes the use of intersection type systems as denotational models instead of the more traditional domain theory, but this choice allows us to build upon the simple type systems studied in Part 2.
Part 3 also proves the basic properties of the denotational semantics using techniques and variations of the techniques introduced in Part 2. We prove the *soundness* of reduction with respect to the denotational semantics by showing that reduction preserves and reflects denotations. We prove *adequacy* of the denotational semantics using a logical-relations style proof with respect to a big-step semantics of the untyped calculus. Finally, with these results in hand, we prove a standardisation theorem, that reduction to weak-head normal form implies the termination of call-by-name evaluation.
To better prepare the reader for Part 3, we made some changes and updates to Part 2. We’ve changed the reduction semantics for the untyped lambda calculus to be the standard one, with unconstrained beta reduction. We also added two new chapters to Part 2. The first proves confluence—a.k.a. the Church-Rosser property—for the untyped lambda calculus. The second presents big-step semantics for call-by-name evaluation, and proves that call-by-name termination implies the reduction to weak-head normal form.
Finally, we also include an Appendix with a single chapter, which proves the substitution lemma for the untyped lambda calculus. We opted to place this chapter an Appendix, and not in Part 2, because we already discuss substitution for the simply-typed lambda calculus, and we feel it would not be particularly enlightening for students to work through the proofs, especially since the ratio of insight to lines of code is rather low.

20
index.md
View file

@ -38,16 +38,16 @@ Pull requests are encouraged.
- [Bisimulation]({{ site.baseurl }}/Bisimulation/): Relating reductions systems
- [Inference]({{ site.baseurl }}/Inference/): Bidirectional type inference
- [Untyped]({{ site.baseurl }}/Untyped/): Untyped lambda calculus with full normalisation
- [Confluence]({{ site.baseurl }}/Confluence/): Confluence of untyped lambda calculus 🚧
- [BigStep]({{ site.baseurl }}/BigStep/): Big-step semantics of untyped lambda calculus 🚧
- [Confluence]({{ site.baseurl }}/Confluence/): Confluence of untyped lambda calculus
- [BigStep]({{ site.baseurl }}/BigStep/): Big-step semantics of untyped lambda calculus
## Part 3: Denotational Semantics
- [Denotational]({{ site.baseurl }}/Denotational/): Denotational semantics of untyped lambda calculus 🚧
- [Compositional]({{ site.baseurl }}/Compositional/): The denotational semantics is compositional 🚧
- [Soundness]({{ site.baseurl }}/Soundness/): Soundness of reduction with respect to denotational semantics 🚧
- [Adequacy]({{ site.baseurl }}/Adequacy/): Adequacy of denotational semantics with respect to operational semantics 🚧
- [ContextualEquivalence]({{ site.baseurl }}/ContextualEquivalence/): Denotational equality implies contextual equivalence 🚧
- [Denotational]({{ site.baseurl }}/Denotational/): Denotational semantics of untyped lambda calculus
- [Compositional]({{ site.baseurl }}/Compositional/): The denotational semantics is compositional
- [Soundness]({{ site.baseurl }}/Soundness/): Soundness of reduction with respect to denotational semantics
- [Adequacy]({{ site.baseurl }}/Adequacy/): Adequacy of denotational semantics with respect to operational semantics
- [ContextualEquivalence]({{ site.baseurl }}/ContextualEquivalence/): Denotational equality implies contextual equivalence
## Appendix
@ -106,11 +106,9 @@ Pull requests are encouraged.
[IU-2020]: https://jsiek.github.io/B522-PL-Foundations/
[SFPL-Meetup-2020]: http://meet.meetup.com/wf/click?upn=ZDzXt-2B-2BZmzYir6Bq5X7vEQ2iNYdgjN9-2FU9nWKp99AU8rZjrncUsSYODqOGn6kV-2BqW71oirCo-2Bk8O1q2FtDFhYZR-2B737CPhNWBjt58LuSRC-2BWTj61VZCHquysW8z7dVtQWxB5Sorl3chjZLDptP70L7aBZL14FTERnKJcRQdrMtc-3D_IqHN4t3hH47BvE1Cz0BakIxV4odHudhr6IVs-2Fzslmv-2FBuORsh-2FwQmOxMBdyMHsSBndQDQmt47hobqsLp-2Bm04Y9LwgV66MGyucsd0I9EgDEUB-2FjzdtSgRv-2Fxng8Pgsa3AZIEYILOhLpQ5ige5VFYTEHVN1pEqnujCHovmTxJkqAK9H-2BIL15-2FPxx97RfHcz7M30YNyqp6TOYfgTxyUHc6lufYKFA75Y7MV6MeDJMxw9-2FYUxR6CEjdoagQBmaGkBVzN
[UW-2019]: https://cs.uwaterloo.ca/~plragde/842/
[UT-2020]: https://www.cs.utexas.edu/~wcook/Courses/386L/Sp2020-GradPL.pdf
[UT-2020]: https://www.cs.utexas.edu/~wcook/Courses/386L/Sp2020-GradPL.pdf
[BHAM-2019]: https://www.cs.bham.ac.uk/internal/modules/2019/06-26943/
[EUSA-2020]: https://www.eusa.ed.ac.uk/representation/campaigns/teachingawards2020/
[SBMF]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
[SCP]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#scf
[NextJournal]: https://nextjournal.com/plfa/ToC
[NextJournal]: https://nextjournal.com/plfa/ToC