Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Tue 5 Sep 2017 13:00 - 13:22 at L1 - Foundations of Higher-Order Programming Chair(s): Gabriel Scherer

We present a general methodology of proving decidability of equational theory of programming language concepts in the framework of second-order algebraic theories of Fiore, Hur and Mahmoud. We propose a Haskell-based analysis tool \SOL, Second-Order Laboratory, which assists the proofs of confluence and strong normalisation of computation rules derived from second-order algebraic theories.

To cover various examples in programming language theory, we combine and extend both syntactical and semantical results of second-order computation in non-trivial manner. In particular, our choice of Yokoyama's deterministic second-order patters as a syntactic construct of rules is important to cover a wide range of examples, such as
Hasegawa's linear \lmd-calculus. We demonstrate how to prove decidability of various algebraic theories in the literature. It includes the equational theories of monad and computational \lmd-calculi, Staton's theory of reading and writing bits, Plotkin and Power's theory of states, and Stark's theory of \pi-calculus.

Tue 5 Sep

Displayed time zone: Belfast change

13:00 - 14:30
Foundations of Higher-Order ProgrammingResearch Papers at L1
Chair(s): Gabriel Scherer Northeastern University
13:00
22m
Talk
How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation
Research Papers
Makoto Hamana Gunma University, Japan
DOI
13:22
22m
Talk
A Relational Logic for Higher-Order Programs
Research Papers
Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Spain, Marco Gaboardi University at Buffalo, SUNY, USA, Deepak Garg MPI-SWS, Germany, Pierre-Yves Strub École Polytechnique, n.n.
DOI
13:45
22m
Talk
Foundations of Strong Call by Need
Research Papers
Thibaut Balabonski LRI, France / University of Paris-Sud, France, Pablo Barenbaum University of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, Eduardo Bonelli CONICET, Argentina / Universidad Nacional de Quilmes, Argentina, Delia Kesner Université de Paris, CNRS, IRIF, France
DOI
14:07
22m
Talk
No-Brainer CPS Conversion
Research Papers
Milo Davis Northeastern University, USA, William Meehan Northeastern University, USA, Olin Shivers Northeastern University, USA
DOI