Sciweavers

TYPES
2007
Springer
14 years 5 months ago
Characterising Strongly Normalising Intuitionistic Sequent Terms
This paper gives a characterisation, via intersection types, of the strongly normalising terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the ...
José Espírito Santo, Silvia Ghilezan...
TYPES
2007
Springer
14 years 5 months ago
Working with Mathematical Structures in Type Theory
Claudio Sacerdoti Coen, Enrico Tassi
TYPES
2007
Springer
14 years 5 months ago
In the Search of a Naive Type Theory
Agnieszka Kozubek, Pawel Urzyczyn
TYPES
2007
Springer
14 years 5 months ago
A Declarative Language for the Coq Proof Assistant
This paper presents a new proof language for the Coq proof assistant. This language uses the declarative style. It aims at providing a simple, natural and robust alternative to the...
Pierre Corbineau
TYPES
2007
Springer
14 years 5 months ago
On Normalization by Evaluation for Object Calculi
We present a procedure for computing normal forms of terms in Abadi and Cardelli’s functional object calculus. Even when equipped with simple types, terms of this calculus are no...
Jan Schwinghammer
TYPES
2007
Springer
14 years 5 months ago
Attributive Types for Proof Erasure
Abstract. Proof erasure plays an essential role in the paradigm of programming with theorem proving. In this paper, we introduce a form of attributive types that carry an attribute...
Hongwei Xi
TYPES
2007
Springer
14 years 5 months ago
A Logic for Parametric Polymorphism with Effects
Rasmus Ejlers Møgelberg, Alex Simpson
TYPES
2007
Springer
14 years 5 months ago
Dependently Sorted Logic
Abstract. We propose syntax and semantics for systems of intuitionistic and classical first order dependently sorted logic, with and withlity, retaining type dependency, but other...
João Filipe Belo
TYPES
2007
Springer
14 years 5 months ago
Intuitionistic vs. Classical Tautologies, Quantitative Comparison
We consider propositional formulas built on implication. The size of a formula is the number of occurrences of variables in it. We assume that two formulas which differ only in th...
Antoine Genitrini, Jakub Kozik, Marek Zaionc