Lecture Notes in Computer Science

Subtyping with singleton types.- A subtyping for the Fisher-Honsell-Mitchell lambda calculus of objects.- The Girard Translation extended with recursion.- Decidability of higher-order subtyping with intersection types.- A ?-calculus structure isomorphic to Gentzen-style sequent calculus structure.- Usability: formalising (un)definedness in typed lambda calculus.- Lambda representation of operations between different term algebras.- Semi-unification and generalizations of a particularly simple form.- A mixed linear and non-linear logic: Proofs, terms and models.- Cut free formalization of logic with finitely many variables. Part I..- How to lie without being (easily) convicted and the lengths of proofs in propositional calculus.- Monadic second-order logic and linear orderings of finite structures.- First-order spectra with one binary predicate.- Monadic logical definability of NP-complete problems.- Logics for context-free languages.- Log-approximable minimization problems on random inputs.- Convergence and 0-1 laws for L ?,? k under arbitrary measures.- Is first order contained in an initial segment of PTIME?.- Logic programming in Tau Categories.- Reasoning and rewriting with set-relations I: Ground completeness.- Resolution games and non-liftable resolution orderings.- On existential theories of list concatenation.- Completeness of resolution for definite answers with case analysis.- Subrecursion as a basis for a feasible programming language.- A sound metalogical semantics for input/output effects.- An intuitionistic modal logic with applications to the formal verification of hardware.- Towards machine-checked compiler correctness for higher-order pure functional languages.- Powerdomains, powerstructures and fairness.- Canonical forms for data-specifications.- An algebraic view of structural induction.- On the interpretation of type theory in locally cartesian closed categories.- Algorithmic aspects of propositional tense logics.- Stratified default theories.- A homomorphism concept for ?-regularity.- Ramified recurrence and computational complexity II: Substitution and poly-space.- General form recursive equations I.- Modal logics preserving admissible for S4 inference rules.- A bounded set theory with Anti-Foundation Axiom and inductive definability.