LICS
2010
IEEE
13 years 11 months ago
2010
IEEE
—We design an intuitionistic predicate logic that supports a limited amount of classical reasoning, just enough to prove a variant of Markov’s principle suited for predicate lo...
LICS
2010
IEEE
13 years 11 months ago
2010
IEEE
This work belongs to a wider effort aimed at eliminating syntactic bureaucracy from proof systems. In this paper, we present a novel cut elimination procedure for classical propos...
LICS
2010
IEEE
13 years 11 months ago
2010
IEEE
—There are two usual ways to describe equality in a dependent typing system, one that uses an external notion of computation like beta-reduction, and one that introduces a typed ...
LICS
2010
IEEE
13 years 11 months ago
2010
IEEE
Abstract—Polarized logic is the logic of values and continuations, and their interaction through continuation-passing style. The main limitations of this logic are the limitation...
LICS
2010
IEEE
13 years 11 months ago
2010
IEEE
Abstract—Maximality is a desirable property of paraconsistent logics, motivated by the aspiration to tolerate inconsistencies, but at the same time retain as much as possible fro...
LICS
2010
IEEE
13 years 11 months ago
2010
IEEE
—We provide a syntactic analysis of contextual preorder and equivalence for a polymorphic programming language with effects. Our approach applies uniformly across a range of alge...
LICS
2010
IEEE
13 years 11 months ago
2010
IEEE
We solve the open problem of the decidability of Boolean BI logic (BBI), which can be considered as the core of separation and spatial logics. For this, we define a complete phas...