CSL
2008
Springer
13 years 12 months ago
2008
Springer
Abstract. This paper shows undecidability of type-checking and typeinference problems in domain-free typed lambda-calculi with existential types: a negation and conjunction fragmen...
CSL
2010
Springer
13 years 12 months ago
2010
Springer
It is standard to regard the intuitionistic restriction of a classical logic as increasing the expressivity of the logic because the classical logic can be adequately represented i...
CSL
2010
Springer
13 years 12 months ago
2010
Springer
Abstract. The relationship between automata and logics has been investigated since the 1960s. In particular, it was shown how to determine, given an automaton, whether or not it is...
CSL
2010
Springer
13 years 12 months ago
2010
Springer
Abstract. We present a symbolic framework, based on a modular operational semantics, for formalizing different notions of compromise relevant for the analysis of cryptographic prot...
CSL
2010
Springer
13 years 12 months ago
2010
Springer
Deduction modulo consists in presenting a theory through rewrite rules to support automatic and interactive proof search. It induces proof search methods based on narrowing, such a...
CSL
2010
Springer
13 years 12 months ago
2010
Springer
CSL
2010
Springer
13 years 12 months ago
2010
Springer
Abstract. Graded path quantifiers have been recently introduced and investigated as a useful framework for generalizing standard existential and universal path quantifiers in the b...
CSL
2010
Springer
13 years 12 months ago
2010
Springer
Abstract. Recent analysis of sequential algorithms resulted in their axiomatization and in a representation theorem stating that, for any sealgorithm, there is an abstract state ma...
CSL
2010
Springer
13 years 12 months ago
2010
Springer
Abstract. We prove "untyping" theorems: in some typed theories (semirings, Kleene algebras, residuated lattices, involutive residuated lattices), typed equations can be d...
CSL
2010
Springer
13 years 12 months ago
2010
Springer
We shall discuss several situations in which it is possible to extract from a proof, be it a proof in a first-order theory or a propositional proof, some feasible computational inf...