Encontrados 16 documentos, a visualizar página 1 de 2
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 ...
A calculus of multiary sequent terms
Espírito Santo, José; Pinto, Luís F.Multiary sequent terms were originally introduced as a tool for proving termination of permutative conversions in cut-free sequent calculus. This work develops the language of multiary sequent terms into a term calculus for the computational (Curry-Howard) interpretation of a fragment of sequent calculus with cuts and cut-elimination rules. The system, named generalised multiary lambda-calculus, is a rich exten...
Relating sequent calculi for bi-intuitionistic propositional logic
Pinto, Luís F.; Uustalu, TarmoBi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication. It is sometimes presented as a symmetric constructive subsystem of classical logic. In this paper, we compare three sequent calculi for bi-intuitionistic propositional logic: (1) a basic standard-style sequent calculus that restricts the premises of implication-right and exclusion-le...
Proof search and counter-model construction for bi-intuitionistic propositional...
Pinto, Luís F.; Uustalu, TarmoBi-intuitionistic logic is a conservative extension of intuitionistic logic with a connective dual to implication, called exclusion. We present a sound and complete cut-free labelled sequent calculus for bi-intuitionistic propositional logic, BiInt, following S. Negri's general method for devising sequent calculi for normal modal logics. Although it arises as a natural formalization of the Kripke se...
Structural proof theory as rewriting
Espírito Santo, José; Frade, M. J.; Pinto, Luís F.The multiary version of the $\lambda$-calculus with generalized applications integrates smoothly both a fragment of sequent calculus and the system of natural deduction of von Plato. It is equipped with reduction rules (corresponding to cut-elimination/normalisation rules) and permutation rules, typical of sequent calculus and of natural deduction with generalised elimination rules. We argue that this system is...
Model checking embedded systems with PROMELA
Ribeiro, Óscar R.; Fernandes, João M.; Pinto, Luís F.Comunicação apresentada ao IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2005), 12, Washington, 2005. ; The design process for embedded systems can benefit from the usage of formal methods, if some properties of the systems are checked, before design and implementation decisions are accomplished. This paper presents a model checking approach using the Spin tool, ...
Type-based termination of recursive definitions
Barthe, Gilles; Frade, M. J.; Giménez, E.; Pinto, Luís F.; Uustalu, TarmoThis paper introduces "lambda-hat", a simply typed lambda calculus supporting inductive types and recursive function definitions with termination ensured by types. The system is shown to enjoy subject reduction, strong normalisation of typable terms and to be stronger than a related system "lambda-G" in which termination is ensured by a syntactic guard condition. The system can, at will, be extended to ...
Confluence and strong normalisation of the generalised multiary lambda-calculus
Espírito Santo, José; Pinto, Luís F.In a previous work we introduced the {\em generalised multiary $\lambda$-calculus} lambda-Jm, an extension of the $\lambda$-calculus where functions can be applied to lists of arguments (a feature which we call "multiarity'') and encompassing "generalised'' eliminations of von Plato. In this paper we prove confluence and strong normalisation of the reduction relations of lambda-Jm. Proofs of these results lif...
Permutative conversions in intuitionistic multiary sequent calculus with cuts
Espírito Santo, José; Pinto, Luís F.This work presents an extension with cuts of Schwichtenberg's multiary sequent calculus. We identify a set of permutative conversions on it, prove their termination and confluence and establish the permutability theorem. We present our sequent calculus as the typing system of the {\em generalised multiary $\lambda$-calculus} lambda-Jm, a new calculus introduced in this work. Lambda-Jm corresponds to an extensio...
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||