Sciweavers

CSL
2005
Springer
13 years 10 months ago
Distributed Control Flow with Classical Modal Logic
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...
Tom Murphy VII, Karl Crary, Robert Harper
CSL
2005
Springer
13 years 10 months ago
Feasible Proofs of Matrix Properties with Csanky's Algorithm
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...
Michael Soltys
CSL
2005
Springer
13 years 10 months ago
A Propositional Proof System for Log Space
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...
Steven Perron
CSL
2005
Springer
13 years 10 months ago
On Deciding Topological Classes of Deterministic Tree Languages
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...
Filip Murlak
CSL
2005
Springer
13 years 10 months ago
Complexity and Intensionality in a Type-1 Framework for Computable Analysis
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...
Branimir Lambov
CSL
2005
Springer
13 years 10 months ago
Light Functional Interpretation
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...
Mircea-Dan Hernest
CSL
2005
Springer
13 years 10 months ago
Towards a Typed Geometry of Interaction
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...
Esfandiar Haghverdi, Philip J. Scott
CSL
2005
Springer
13 years 10 months ago
The Ackermann Award 2005
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...
Erich Grädel, Janos Makowsky, Alexander A. Ra...
CSL
2005
Springer
13 years 10 months ago
L-Nets, Strategies and Proof-Nets
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...
Pierre-Louis Curien, Claudia Faggian