CSL
2005
Springer
14 years 4 months ago
2005
Springer
In previous work we presented a foundational calculus for spatially distributed computing based on intuitionistic modal logic. With the modalities P and Q we were able to capture t...
CSL
2005
Springer
14 years 4 months ago
2005
Springer
We show that Csanky’s fast parallel algorithm for computing the characteristic polynomial of a matrix can be formalized in the logical theory LAP, and can be proved correct in LA...
CSL
2005
Springer
14 years 4 months ago
2005
Springer
The proof system G∗ 0 of the quantified propositional calculus corresponds to NC1 , and G∗ 1 corresponds to P, but no formula-based proof system that corresponds log space rea...
CSL
2005
Springer
14 years 4 months ago
2005
Springer
Abstract. It has been proved by Niwi´nski and Walukiewicz that a deterministic tree language is either Π1 1 -complete or it is on the level Π0 3 of the Borel hierarchy, and that...
CSL
2005
Springer
14 years 4 months ago
2005
Springer
CSL
2005
Springer
14 years 4 months ago
2005
Springer
Implementations of real number computations have largely been unusable in practice because of their very bad performance, especially in comparison to floating point arithmetic imp...
CSL
2005
Springer
14 years 4 months ago
2005
Springer
We give a Natural Deduction formulation of an adaptation of G¨odel’s functional (Dialectica) interpretation to the extraction of (more) efficient programs from (classical) proof...
CSL
2005
Springer
14 years 4 months ago
2005
Springer
Abstract. Girard’s Geometry of Interaction (GoI) develops a mathematical framework for modelling the dynamics of cut-elimination. We introduce a typed version of GoI, called Mult...
CSL
2005
Springer
14 years 4 months ago
2005
Springer
ce, the publication of the abstract of the thesis and the citation in the CSL proceedings, and travel support to attend the conference. The first Ackermann Award is presented at t...
CSL
2005
Springer
14 years 4 months ago
2005
Springer
We consider the setting of L-nets, recently introduced by Faggian and Maurel as a game model of concurrent interaction and based on Girard’s Ludics. We show how L-nets satisfying...