Write a Blog >>
APLAS 2019
Sun 1 - Wed 4 December 2019 Bali, Indonesia
Mon 2 Dec 2019 16:30 - 17:00 at Bali Room - Semantics Chair(s): Atsushi Igarashi

Program calculation, a programming technique to derive efficient programs from naive ones by program transformation, is a challenging activity for program optimization. Tesson et al. have shown that Coq, a popular theorem proof assistant, provides a cheap way to implement a powerful system for verifying correctness of the transformations, but its applications are limited to the calculation of list functions in Theory of Lists. In this paper, we prove more advanced calculation rules in Coq for various recursion schemes, which capture the recursive programs on an arbitrary algebraic datatype. We construct Coq formal proof of all the lemmas and theorems about recursion schemes including histomorphism and futumorphism proposed by Uustalu and Vene. The feature of our proposal is that it is possible to obtain certified runnable programs from definitions written with recursion schemes in Coq scripts. We have succeeded in obtaining a certified runnable program to compute the n-th Fibonacci number from its histomorphic definition.

Conference Day
Mon 2 Dec

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change

15:30 - 17:00
SemanticsResearch Papers at Bali Room
Chair(s): Atsushi IgarashiKyoto University, Japan
15:30
30m
Talk
Factorization and Normalization, Essentially
Research Papers
Beniamino AccattoliInria & Ecole Polytechnique, Claudia FaggianIRIF, Giulio GuerrieriUniversity of Bath
16:00
30m
Talk
Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion
Research Papers
Masayuki MizunoTohoku University , Eijiro SumiiTohoku University
16:30
30m
Talk
Recursion Schemes in Coq
Research Papers
Kosuke MurataKyushu Institute of Technology , Kento EmotoKyushu Institute of Technology