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.

Mon 2 Dec
Times are displayed in time zone: (GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi change

15:30 - 17:00: Research Papers - Semantics at Bali Room
Chair(s): Atsushi IgarashiKyoto University, Japan
aplas-2019-papers15:30 - 16:00
Beniamino AccattoliInria & Ecole Polytechnique, Claudia FaggianIRIF, Giulio GuerrieriUniversity of Bath
aplas-2019-papers16:00 - 16:30
Masayuki MizunoTohoku University , Eijiro SumiiTohoku University
aplas-2019-papers16:30 - 17:00
Kosuke MurataKyushu Institute of Technology , Kento EmotoKyushu Institute of Technology