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.

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 fordata-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.

GPSR Compliance The European Union's (EU) General Product Safety Regulation (GPSR) is a set of rules that requires consumer products to be safe and our obligations to ensure this. If you have any concerns about our products you can contact us on ProductSafety@springernature.com. In case Publisher is established outside the EU, the EU authorized representative is: Springer Nature Customer Service Center GmbH Europaplatz 3 69115 Heidelberg, Germany ProductSafety@springernature.com