Encontrados 25 documentos, a visualizar página 1 de 3
Turing e a normalização
Espírito Santo, José Carlos; Universidade do MinhoAlgumas contribuições de Turing em Lógica dizem respeito àTeoria de Tipos e foram desenvolvidas durante a Segunda Guerra Mundial.Um dos resultados desse trabalho é uma demonstração do teorema da norma-lização para tipos simples, que permaneceu ignorada durante 40 anos. Oresultado de Turing é, portanto, um dos episódios da complicada história da(re)descoberta da normalização.
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 ...
Towards a canonical classical natural deduction system
Espírito Santo, JoséPreprint submitted to Elsevier, 6 July 2012 ; This paper studies a new classical natural deduction system, presented as a typed calculus named lambda-mu- let. It is designed to be isomorphic to Curien and Herbelin's lambda-mu-mu~-calculus, both at the level of proofs and reduction, and the isomorphism is based on the correct correspondence between cut (resp. left-introduction) in sequent calculus, and subst...
Turing e a normalização
Espírito Santo, JoséEm publicação ; Algumas contribuições de Turing em Lógica dizem respeito à Teoria de Tipos e foram desenvolvidas durante a Segunda Guerra Mundial. Um dos resultados desse trabalho é uma demonstração do teorema da normalização para tipos simples, que permaneceu ignorada durante 40 anos. O resultado de Turing é, portanto, um dos episódios da complicada história da (re)descoberta da normalização. ; The part of T...
Characterising strongly normalising intuitionistic terms
Espírito Santo, José; Ivetic, J,; Likavec, SilviaThis paper gives a characterisation, via intersection types, of the strongly normalising proof-terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary lambdal-calculus. The completeness of the typing system is obtained from subject expansion at root position. Next we use our...
Concepções sobre qualidade de ensino em estabelecimentos de ensino superior púb...
Martins, Maria; Oliveira, Teresa; Barros, João Paulo; Espírito Santo, José; Trindade, Vítor; Bonito, JorgeEste estudo tem como objectivos conhecer e comparar as concepções sobre a qualidade de ensino de docentes e estudantes de três estabelecimentos públicos de ensino superior da região do Alentejo (Portugal) e, no caso dos docentes, conhecer também o que eles sugerem para melhorar a qualidade de ensino nos cursos e nas instituições em que leccionam. Trata-se de um estudo qualitativo, que inclui uma análise de cont...
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...
A note on preservation of strong normalisation in the lambda-calculus
Espírito Santo, JoséAn auxiliary notion of reduction ρ on the λ-terms preserves strong normalisation if all strongly normalising terms for β are also strongly normalising for β∪ρ.Wegive a sufficient condition for ρ to preserve strong normalisation. As an example of application, we check easily the sufficient condition for Regnier’s σ-reduction rules and the ‘‘assoc’’-reduction rule inspired by calculi with let-expressions. This gi...
Concepções sobre qualidade de ensino em estabelecimentos de ensino superior púb...
Martins, Maria José D.; Oliveira, Teresa; Barros, João Paulo; Espírito Santo, José; Trindade, Vítor; Bonito, JorgeEste estudo tem como objectivos conhecer e comparar as concepções sobre a qualidade de ensino de docentes e estudantes de três estabelecimentos públicos de ensino superior da região do Alentejo (Portugal) e, no caso dos docentes, conhecer também o que eles sugerem para melhorar a qualidade de ensino nos cursos e nas instituições em que leccionam. Trata-se de um estudo qualitativo, que inclui uma análise de cont...
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||