Formal verification of functional programs performing infinite input/output

Masayuki Mizuno, Eijiro Sumii

Research output: Contribution to journalArticlepeer-review

Abstract

Although formal verification of compilers is extensively studied, compilers for higher-order functional programming languages with side effects such as input and output are rarely verified. This is due to the difficulty of formalizing the semantics of programs performing infinite input and output. We have mechanically verified the K-normalization of call-by-value higher-order functional programs with recursive functions, pairs, and external function calls that can possibly cause side effects, by the Coq proof assistant. K-normalization is a program transformation that gives explicit names to all subexpressions via let-expressions. Its for-malization is non-trivial because of the manipulation of bindings. We defined the meanings of programs as infinite sequences of external function calls, using coinductive big-step operational semantics. We also adopted de Bruijn indices by comparison with other techniques to represent bindings.

Original languageEnglish
Pages (from-to)114-119
Number of pages6
JournalComputer Software
Volume34
Issue number2
Publication statusPublished - 2017 May 1

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Formal verification of functional programs performing infinite input/output'. Together they form a unique fingerprint.

Cite this