Computer Science Logic: 8th Workshop, CSL ’94 Kazimierz, Poland, September 25–30, 1994 Selected Papers

David Aspinall (auth.), Leszek Pacholski, Jerzy Tiuryn (eds.)3540600175, 9783540600176

This volume contains revised refereed versions of the best papers presented during the CSL ’94 conference, held in Kazimierz, Poland in September 1994; CSL ’94 is the eighth event in the series of workshops held for the third time as the Annual Conference of the European Association for Computer Science Logic.
The 38 papers presented were selected from a total of 151 submissions. All important aspects of the methods of mathematical logic in computer science are addressed: lambda calculus, proof theory, finite model theory, logic programming, semantics, category theory, and other logical systems. Together, these papers give a representative snapshot of the area of logical foundations of computer science.

---

Table of contents :
Subtyping with singleton types….Pages 1-15
A subtyping for the Fisher-Honsell-Mitchell lambda calculus of objects….Pages 16-30
The Girard Translation extended with recursion….Pages 31-45
Decidability of higher-order subtyping with intersection types….Pages 46-60
A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure….Pages 61-75
Usability: formalising (un)definedness in typed lambda calculus….Pages 76-90
Lambda representation of operations between different term algebras….Pages 91-105
Semi-unification and generalizations of a particularly simple form….Pages 106-120
A mixed linear and non-linear logic: Proofs, terms and models….Pages 121-135
Cut free formalization of logic with finitely many variables. Part I…..Pages 136-150
How to lie without being (easily) convicted and the lengths of proofs in propositional calculus….Pages 151-162
Monadic second-order logic and linear orderings of finite structures….Pages 163-176
First-order spectra with one binary predicate….Pages 177-189
Monadic logical definability of NP-complete problems….Pages 190-204
Logics for context-free languages….Pages 205-216
Log-approximable minimization problems on random inputs….Pages 217-227
Is first order contained in an initial segment of PTIME?….Pages 228-241
Logic programming in Tau Categories….Pages 242-248
Reasoning and rewriting with set-relations I: Ground completeness….Pages 249-263
Resolution games and non-liftable resolution orderings….Pages 264-278
On existential theories of list concatenation….Pages 279-293
Completeness of resolution for definite answers with case analysis….Pages 294-308
Subrecursion as a basis for a feasible programming language….Pages 309-323
A sound metalogical semantics for input/output effects….Pages 324-338
An intuitionistic modal logic with applications to the formal verification of hardware….Pages 339-353
Towards machine-checked compiler correctness for higher-order pure functional languages….Pages 354-368
Powerdomains, powerstructures and fairness….Pages 369-381
Canonical forms for data-specifications….Pages 382-396
An algebraic view of structural induction….Pages 397-411
On the interpretation of type theory in locally cartesian closed categories….Pages 412-426
Algorithmic aspects of propositional tense logics….Pages 427-441
Stratified default theories….Pages 442-455
A homomorphism concept for ω-regularity….Pages 456-470
Ramified recurrence and computational complexity II: Substitution and poly-space….Pages 471-485
General form recursive equations I….Pages 486-500
Modal logics preserving admissible for S 4 inference rules….Pages 501-511
A bounded set theory with Anti-Foundation Axiom and inductive definability….Pages 512-526
….Pages 527-541