3 papers
cs.LO2023
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…
math.LO2019
The Russell-Prawitz embedding and the atomization of universal instantiation
José Espírito Santo, Gilda Ferreira
Given the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system F_at, we study directly in sy…
cs.LO2016
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…