Continuations, proofs and tests

TL;DR

This paper explores the concept of tests in intuitionistic logic inspired by Girard, developing a complete deductive system that effectively handles continuations and supports both Call by Value and Call by Name translations.

Contribution

It introduces a novel notion of tests for intuitionistic logic and provides a complete deductive system that unifies handling of continuations in different evaluation strategies.

Findings

Developed a complete deductive system for tests in intuitionistic logic

Demonstrated the system's effectiveness with Call by Value and Call by Name translations

Enhanced understanding of continuation handling in functional programming

Abstract

Continuation Passing Style (CPS) is one of the most important issues in the field of functional programming languages, and the quest for a primitive notion of types for continuation is still open. Starting from the notion of ``test'' proposed by Girard, we develop a notion of test for intuitionistic logic. We give a complete deductive system for tests and we show that it is good to deal with ``continuations''. In particular, in the proposed system it is possible to work with Call by Value and Call by Name translations in a uniform way.