TCS

2011

13 years 5 months ago
2011

We give a semantic account of the execution time (i.e. the number of cut elimination steps leading to the normal form) of an untyped MELL net. We ﬁrst prove that: 1) a net is he...

BSL

2006

13 years 10 months ago
2006

We give a self-contained and streamlined version of the classification of the provably computable functions of PA. The emphasis is put on illuminating as good as seems possible th...

CORR

2008

Springer

13 years 10 months ago
2008

Springer

As an attempt to uncover the topological nature of composition of strategies in game semantics, we present a "topological" game for Multiplicative Additive Linear Logic ...

AIML

2006

13 years 11 months ago
2006

We see a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination the axioms d, t, b, 4, 5. They employ a form of deep inference ...

TYPES

1998

Springer

14 years 2 months ago
1998

Springer

We define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theo...

ICFP

2000

ACM

14 years 2 months ago
2000

ACM

We review the close relationship between abstract machines for (call-by-name or call-by-value) λ-calculi (extended with Felleisen’s C) and sequent calculus, reintroducing on the...

CSL

2001

Springer

14 years 2 months ago
2001

Springer

We introduce the calculus of structures: it is more general than the sequent calculus and it allows for cut elimination and the subformula property. We show a simple extension of m...

CSL

2003

Springer

14 years 3 months ago
2003

Springer

System SKS is a set of rules for classical propositional logic presented in the calculus of structures. Like sequent systems and unlike natural deduction systems, it has an explici...

PADL

2004

Springer

14 years 3 months ago
2004

Springer

Gentzen’s Hauptsatz – cut elimination theorem – in sequent calculi reveals a fundamental property on logic connectives in various logics such as classical logic and intuition...

TLCA

2005

Springer

14 years 3 months ago
2005

Springer

Cut elimination is a central result of the proof theory. This paper proposes a new approach for proving the theorem for Gentzen’s intuitionistic sequent calculus LJ, that relies ...