Typed lambda calculi and applications

Meer over het boek

This book explores a variety of advanced topics in logic, type systems, and computational theory. It begins with explicit substitutions and transitions to the relationship between proof-nets and linear logic type systems, particularly in the context of polynomial time computing. The work delves into strong normalization and equi-(co)inductive types, alongside semantics for intuitionistic arithmetic through Tarski games with retractable moves. It introduces the safe lambda calculus and intuitionistic refinement calculus, as well as computation by prophecy. An arithmetical proof of strong normalization for the lambda calculus is presented, along with the embedding of pure type systems in the lambda-pi-calculus modulo. The text further discusses continuation-passing style and strong normalization in intuitionistic sequent calculi, and models for the finitary linear pi-calculus. It examines differential structures in models of multiplicative biadditive intuitionistic linear logic and the completeness of the omega rule in the lambda-calculus. Other topics include weakly distributive domains, initial algebra semantics, substructural type systems, the inhabitation problem for rank two intersection types, extensional rewriting, higher-order logic programming languages with constraints, and full abstraction for symmetric interaction combinators. The book concludes with insights on session typing systems for higher-order mobile processe