Simona Ronchi della Rocca Livres

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

The book contains a completely new presentation of classical results in the field of Lambda Calculus, together with new results. The text is unique in that it presents a new calculus (Parametric Lambda Calculus) which can be instantiated to obtain already known lambda-calculi. Some properties, which in the literature have been proved separately for different calculi, can be proved once for the Parametric one. The lambda calculi are presented from a Computer Science point of view, with a particular emphasis on their semantics, both operational and denotational.