xThe data center, from which the conference websites are hosted, is currently experiencing power issues. Our colleagues are working hard to resolve the issue and keep downtime to a minimum.
ICFP 2021
Sun 22 - Sat 28 August 2021
Tue 24 Aug 2021 20:30 - 20:45 at ICFP Talks - Session 4
Wed 25 Aug 2021 08:30 - 08:45 at ICFP Talks - Session 4

Consider two widely used definitions of equality. That of Leibniz: one value equals another if any predicate that holds of the first holds of the second. And that of Martin-Löf: the type identifying one value with another is occupied if the two values are identical. The former dates back several centuries, while the latter is widely used in proof systems such as Agda and Coq. Here we show that the two definitions are isomorphic: we can convert any proof of Leibniz equality to one of Martin-Löf identity and vice versa, and each conversion followed by the other is the identity. One direction of the isomorphism depends crucially on values of the type corresponding to Leibniz equality satisfying functional extensionality and Reynolds’ notion of parametricity. The existence of the conversions is widely known (meaning that if one can prove one equality then one can prove the other), but that the two conversions form an isomorphism (internally) in the presence of parametricity and functional extensionality is, we believe, new. Our result is a special case of a more general relation that holds between inductive families and their Church encodings. Our proofs are given inside type theory, rather than meta-theoretically. Our paper is a literate Agda script.

Tue 24 Aug

Displayed time zone: Seoul change

19:00 - 20:45
19:00
15m
Talk
How to design co-programs (JFP Presentation)
Research Papers
Jeremy Gibbons Department of Computer Science, University of Oxford
Link to publication DOI Media Attached
19:15
15m
Talk
A Theory of Higher-Order Subtyping with Type Intervals
Research Papers
Sandro Stucki Chalmers | University of Gothenburg, Paolo G. Giarrusso Delft University of Technology
DOI Pre-print Media Attached
19:30
15m
Talk
Typed dataspace actors (JFP Presentation)
Research Papers
Sam Caldwell Northeastern University, Tony Garnock-Jones Northeastern University, USA, Matthias Felleisen Northeastern University
Link to publication DOI Media Attached
19:45
15m
Talk
An Existential Crisis Resolved: Type Inference for First-Class Existential TypesDistinguished Paper
Research Papers
Richard A. Eisenberg Tweag, Guillaume Duboc ENS Lyon, Stephanie Weirich University of Pennsylvania, Daniel Lee
DOI Media Attached
20:00
15m
Talk
Proof-directed program transformation: A functional account of efficient regular expression matching (JFP Presentation)
Research Papers
Andrzej Filinski DIKU, University of Copenhagen
Link to publication DOI Media Attached
20:15
15m
Talk
Distributing Intersection and Union Types with Splits and Duality (Functional Pearl)
Research Papers
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI Pre-print Media Attached
20:30
15m
Talk
Leibniz equality is isomorphic to Martin-Löf identity, parametrically (JFP Presentation)
Research Papers
Dominique Devriese Vrije Universiteit Brussel, Andreas Abel Gothenburg University, Jesper Cockx TU Delft, Amin Timany Aarhus University, Philip Wadler University of Edinburgh
Link to publication DOI Media Attached

Wed 25 Aug

Displayed time zone: Seoul change

07:00 - 08:45
Session 4Research Papers at ICFP Talks
07:00
15m
Talk
How to design co-programs (JFP Presentation)
Research Papers
Jeremy Gibbons Department of Computer Science, University of Oxford
Link to publication DOI Media Attached
07:15
15m
Talk
A Theory of Higher-Order Subtyping with Type Intervals
Research Papers
Sandro Stucki Chalmers | University of Gothenburg, Paolo G. Giarrusso Delft University of Technology
DOI Pre-print Media Attached
07:30
15m
Talk
Typed dataspace actors (JFP Presentation)
Research Papers
Sam Caldwell Northeastern University, Tony Garnock-Jones Northeastern University, USA, Matthias Felleisen Northeastern University
Link to publication DOI Media Attached
07:45
15m
Talk
An Existential Crisis Resolved: Type Inference for First-Class Existential TypesDistinguished Paper
Research Papers
Richard A. Eisenberg Tweag, Guillaume Duboc ENS Lyon, Stephanie Weirich University of Pennsylvania, Daniel Lee
DOI Media Attached
08:00
15m
Talk
Proof-directed program transformation: A functional account of efficient regular expression matching (JFP Presentation)
Research Papers
Andrzej Filinski DIKU, University of Copenhagen
Link to publication DOI Media Attached
08:15
15m
Talk
Distributing Intersection and Union Types with Splits and Duality (Functional Pearl)
Research Papers
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI Pre-print Media Attached
08:30
15m
Talk
Leibniz equality is isomorphic to Martin-Löf identity, parametrically (JFP Presentation)
Research Papers
Dominique Devriese Vrije Universiteit Brussel, Andreas Abel Gothenburg University, Jesper Cockx TU Delft, Amin Timany Aarhus University, Philip Wadler University of Edinburgh
Link to publication DOI Media Attached