Explicit weakening

Philip Wadler

doi:10.4204/EPTCS.413.2

Explicit weakening

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

Abstract

I present a novel formulation of substitution, where facts about substitution that previously required tens or hundreds of lines to justify in a proof assistant now follow immediately - they can be justified by writing the four letters "refl". The paper is an executable literate Agda script, and source of the paper is available as an artifact in the file Weaken.lagda.md.

Not all consequences of the pandemic have been awful. For the last three years, I've had the great pleasure of meeting with Peter Thiemann and Jeremy Siek for a couple of hours every week, via Zoom, exploring topics including core calculi, gradual typing, and formalisation in Agda. The work reported here arose from those discussions, and is dedicated to Peter on the occasion of his 60th birthday.

Original language	English
Title of host publication	A Second Soul
Subtitle of host publication	Celebrating the Many Languages of Programming - Festschrift in Honor of Peter Thiemann's Sixtieth Birthday
Editors	Annette Bieniusa, Markus Degen, Stefan Wehr
Publisher	Open Publishing Association
Pages	15-26
Number of pages	12
DOIs	https://doi.org/10.4204/EPTCS.413.2
Publication status	Published - 30 Nov 2024
Event	A Second Soul: Celebrating the Many Languages of Programming - Festschrift in Honor of Peter Thiemann's Sixtieth Birthday - Freiburg, Germany Duration: 30 Aug 2024 → 30 Aug 2024 https://cgi.cse.unsw.edu.au/~eptcs/content.cgi?PT2024

Publication series

Name	Electronic Proceedings in Theoretical Computer Science
Publisher	Open Publishing Association
Volume	413
ISSN (Print)	2075-2180

Symposium

Symposium	A Second Soul
Country/Territory	Germany
City	Freiburg
Period	30/08/24 → 30/08/24
Internet address	https://cgi.cse.unsw.edu.au/~eptcs/content.cgi?PT2024

Access to Document

10.4204/EPTCS.413.2Licence: Creative Commons: Attribution (CC-BY)

WadlerEPTCS2024ExplicitWeakeningFinal published version, 192 KBLicence: Creative Commons: Attribution (CC-BY)

https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?PT2024.2Licence: Creative Commons: Attribution (CC-BY)

Cite this

@inbook{6b9767ac716049b798a2071a65f26e73,

title = "Explicit weakening",

abstract = "I present a novel formulation of substitution, where facts about substitution that previously required tens or hundreds of lines to justify in a proof assistant now follow immediately - they can be justified by writing the four letters {"}refl{"}. The paper is an executable literate Agda script, and source of the paper is available as an artifact in the file Weaken.lagda.md. Not all consequences of the pandemic have been awful. For the last three years, I've had the great pleasure of meeting with Peter Thiemann and Jeremy Siek for a couple of hours every week, via Zoom, exploring topics including core calculi, gradual typing, and formalisation in Agda. The work reported here arose from those discussions, and is dedicated to Peter on the occasion of his 60th birthday.",

author = "Philip Wadler",

year = "2024",

month = nov,

day = "30",

doi = "10.4204/EPTCS.413.2",

language = "English",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "Open Publishing Association",

pages = "15--26",

editor = "Annette Bieniusa and Markus Degen and Stefan Wehr",

booktitle = "A Second Soul",

address = "Australia",

note = "A Second Soul : Celebrating the Many Languages of Programming - Festschrift in Honor of Peter Thiemann's Sixtieth Birthday ; Conference date: 30-08-2024 Through 30-08-2024",

url = "https://cgi.cse.unsw.edu.au/\textasciitilde{}eptcs/content.cgi?PT2024",

}

Wadler, P 2024, Explicit weakening. in A Bieniusa, M Degen & S Wehr (eds), A Second Soul: Celebrating the Many Languages of Programming - Festschrift in Honor of Peter Thiemann's Sixtieth Birthday. Electronic Proceedings in Theoretical Computer Science, vol. 413, Open Publishing Association, pp. 15-26, A Second Soul, Freiburg, Baden-Württemberg, Germany, 30/08/24. https://doi.org/10.4204/EPTCS.413.2

Explicit weakening. / Wadler, Philip.
A Second Soul: Celebrating the Many Languages of Programming - Festschrift in Honor of Peter Thiemann's Sixtieth Birthday. ed. / Annette Bieniusa; Markus Degen; Stefan Wehr. Open Publishing Association, 2024. p. 15-26 (Electronic Proceedings in Theoretical Computer Science; Vol. 413).

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

TY - CHAP

T1 - Explicit weakening

AU - Wadler, Philip

PY - 2024/11/30

Y1 - 2024/11/30

N2 - I present a novel formulation of substitution, where facts about substitution that previously required tens or hundreds of lines to justify in a proof assistant now follow immediately - they can be justified by writing the four letters "refl". The paper is an executable literate Agda script, and source of the paper is available as an artifact in the file Weaken.lagda.md. Not all consequences of the pandemic have been awful. For the last three years, I've had the great pleasure of meeting with Peter Thiemann and Jeremy Siek for a couple of hours every week, via Zoom, exploring topics including core calculi, gradual typing, and formalisation in Agda. The work reported here arose from those discussions, and is dedicated to Peter on the occasion of his 60th birthday.

AB - I present a novel formulation of substitution, where facts about substitution that previously required tens or hundreds of lines to justify in a proof assistant now follow immediately - they can be justified by writing the four letters "refl". The paper is an executable literate Agda script, and source of the paper is available as an artifact in the file Weaken.lagda.md. Not all consequences of the pandemic have been awful. For the last three years, I've had the great pleasure of meeting with Peter Thiemann and Jeremy Siek for a couple of hours every week, via Zoom, exploring topics including core calculi, gradual typing, and formalisation in Agda. The work reported here arose from those discussions, and is dedicated to Peter on the occasion of his 60th birthday.

UR - https://cgi.cse.unsw.edu.au/~eptcs/Published/PT2024/Papers/100/anc/Weaken.lagda.md

UR - https://www.scopus.com/pages/publications/85213382765

U2 - 10.4204/EPTCS.413.2

DO - 10.4204/EPTCS.413.2

M3 - Chapter (peer-reviewed)

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 15

EP - 26

BT - A Second Soul

A2 - Bieniusa, Annette

A2 - Degen, Markus

A2 - Wehr, Stefan

PB - Open Publishing Association

T2 - A Second Soul

Y2 - 30 August 2024 through 30 August 2024

ER -

Explicit weakening

Abstract

Publication series

Symposium

Access to Document

Other files and links

Fingerprint

Cite this