Encontrados 2 documentos, a visualizar página 1 de 1
Monadic translation of classical sequent calculus
Espírito Santo, José; Matthes, Ralph; Nakazawa, Koji; Pinto, Luís F.Em publicação ; We study monadic translations of the call-by-name (cbn) and the call-by-value (cbv) fragments of the classical sequent calculus lambda-mu-mu~ by Curien and Herbelin and give modular and syntactic proofs of strong normalization. The target of the translations is a new meta-language for classical logic, named monadic lambda-mu . It is a monadic reworking of Parigot’s -calculus, where the monad...
A coinductive approach to proof search
Espírito Santo, José; Matthes, Ralph; Pinto, Luís F.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 implicational fragment. We introduce a variant of lambda calculus with potentially infinitely deep terms and a means of expressing alternatives for the description of the “solution spaces” (called Böhm forests), which are a representation of all ...
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||