Computer Science Logic: 14th InternationalWorkshop, CSL 2000 Annual Conference of the EACSL Fischbachau, Germany, August 21 – 26, 2000 Proceedings

Andreas Blass, Yuri Gurevich (auth.), Peter G. Clote, Helmut Schwichtenberg (eds.)3540678956, 9783540678953

This book constitutes the refereed proceedings of the 13th International Workshop on Computer Science Logic, CSL 2000, held in Fischbachau, Germany as the 8th Annual Conference of the EACSL in August 2000. The 28 revised full papers presented together with eight invited papers were carefully reviewed and selected by the program committee. Among the topics covered are automated deduction, theorem proving, categorical logic, term rewriting, finite model theory, higher order logic, lambda and combinatory calculi, computational complexity, logic programing, constraints, linear logic, modal logic, temporal logic, model checking, formal specification, formal verification, program transformation, etc.

---

Table of contents :
Background, Reserve, and Gandy Machines….Pages 1-17
Choiceless Polynomial Time Computation and the Zero-One Law….Pages 18-40
Composition and Submachine Concepts for Sequential ASMs….Pages 41-60
Une tentative malheureuse de construire une structure éliminant rapidement les quanteurs….Pages 61-70
Translating Theory into Practice — Abstract State Machines within Microsoft….Pages 71-71
Choiceless Polynomial Time Logic: Inability to Express….Pages 72-125
Schema Revisited….Pages 126-138
Automated Verification = Graphs, Automata, and Logic….Pages 139-139
A Fully Complete PER Model for ML Polymorphic Types….Pages 140-155
Subtyping with Power Types….Pages 156-171
The Descriptive Complexity of the Fixed-Points of Bounded Formulas….Pages 172-186
Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic….Pages 187-201
Continuous Functionals of Dependent Types and Equilogical Spaces….Pages 202-216
Definability over Linear Constraints….Pages 217-231
Bounded Arithmetic and Descriptive Complexity….Pages 232-246
Independence: Logics and Concurrency….Pages 247-261
Flatness Is Not a Weakness….Pages 262-276
Sequents, Frames, and Completeness….Pages 277-291
Disjunctive Tautologies as Synchronisation Schemes….Pages 292-301
Axiomatizing the Least Fixed Point Operation and Binary Supremum….Pages 302-316
Interactive Programs in Dependent Type Theory….Pages 317-331
Modal Satisfiability Is in Deterministic Linear Space….Pages 332-342
Logic Programming and Co-inductive Definitions….Pages 343-355
A Theory of Explicit Mathematics Equivalent to ID 1 ….Pages 356-370
On the Complexity of Explicit Modal Logics….Pages 371-383
Finite Models and Full Completeness….Pages 384-398
On the Complexity of Combinatorial and Metafinite Generating Functions of Graph Properties in the Computational Model of Blum, Shub and Smale….Pages 399-410
Elimination of Negation in a Logical Framework….Pages 411-426
Discreet Games, Light Affine Logic and PTIME Computation….Pages 427-441
Completeness of Higher-Order Duration Calculus….Pages 442-456
Equational Termination by Semantic Labelling….Pages 457-471
On the Computational Interpretation of Negation….Pages 472-484
From Programs to Games: Invariance and Safety for Bisimulation….Pages 485-496
Logical Relations and Data Abstraction….Pages 497-511
Elementary Choiceless Constructive Analysis….Pages 512-526
On the Logic of the Standard Proof Predicate….Pages 527-541