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

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