POPL 2020 (series) / Research Papers /
SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References
Thu 23 Jan 2020 11:13 - 11:35 at Ile de France II (IDF II) - Types and Effects Chair(s): Dominique Devriese
We propose a framework to study contextual equivalence of programs written in a call-by-value functional language with local integer references. It reduces the problem of contextual equivalence to the problem of non-reachability in a transition system of memory configurations. This reduction is complete for recursion-free programs.
Restricting to programs that do not allocate references inside the body of functions, we encode this non-reachability problem as a constrained Horn clause that can then be checked for satisfiability automatically. Restricting furthermore to a language with finite data-types, we also get a new decidability result for contextual equivalence at any type.
Thu 23 Jan Times are displayed in time zone: Saskatchewan, Central America change
Thu 23 Jan
Times are displayed in time zone: Saskatchewan, Central America change
10:30 - 11:35 | Types and EffectsResearch Papers at Ile de France II (IDF II) Chair(s): Dominique DevrieseVrije Universiteit Brussel | ||
10:30 21mTalk | Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers Research Papers Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław Link to publication DOI Media Attached | ||
10:51 21mTalk | The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects Research Papers Link to publication DOI Media Attached | ||
11:13 21mTalk | SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References Research Papers Guilhem JaberLS2N, Université de Nantes Link to publication DOI Media Attached |