9 citations · 15 across the 7 of their papers we have counts for
7 papers · 1 filter
The Logical Essence of Compiling With Continuations
José Espírito Santo, Filipa Mendes
The essence of compiling with continuations is that conversion to continuation-passing style (CPS) is equivalent to a source language transformation converting to administrative no…
Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
José Espírito Santo, Ralph Matthes, Luís Pinto
The approach to proof search dubbed "coinductive proof search" (CoIPS), and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to…
A note on strong normalization in classical natural deduction
José Espírito Santo
In the context of natural deduction for propositional classical logic, with classicality given by the inference rule reductio ad absurdum, we investigate the De Morgan translation…
A Coinductive Approach to Proof Search through Typed Lambda-Calculi
José Espírito Santo, Ralph Matthes, Luís Pinto
In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inferen…
Confluence for classical logic through the distinction between values and computations
José Espírito Santo, Ralph Matthes, Koji Nakazawa +1
We apply an idea originated in the theory of programming languages - monadic meta-language with a distinction between values and computations - in the design of a calculus of cut-e…
A Coinductive Approach to Proof Search
José Espírito Santo, Ralph Matthes, Luís Pinto
We propose to study proof search from a coinductive point of view. In this paper, we consider intuitionistic logic and a focused system based on Herbelin's LJT for the implicationa…
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
Jose Espirito Santo, Ralph Matthes, Luis Pinto
The intuitionistic fragment of the call-by-name version of Curien and Herbelin's λ\_mu\_{mu}-calculus is isolated and proved strongly normalising by means of an embedding into the…