Types and programing languages
The book addresses two main audiences: graduate students and researchers specializing in programming languages and type theory, and graduate students and mature undergraduates from all areas of computer science who want an introduction to key concepts in the theory of programming languages. A primary aim is coverage of core topics, including basic operational semantics and associated proof techniques, the untyped lambda-calculus, simple type systems, universal and existential polymorphism, type reconstruction, subtyping, bounded quantification, recursive types, and type operators, with shorter discussions of numerous other topics. A second main goal is pragmatism. The book concentrates on the use of type systems in programming languages, at the expense of some topics (such as denotational semantics) that probably would be included in a more mathematical text on typed lambda-calculi. Part 1 of the book discusses untyped systems. Basic concepts of abstract syntax, inductive definitions and proofs, inference rules, and operational semantics are introduced first in the setting of a very simple language of numbers and booleans, the repeated for the untyped lambda-calculus. Part 2 covers the simply typed lambda-calculus and a variety of basic language features such as products, sums, records, variants, references, and exceptions. A preliminary chapter on typed arithmetic expressions provides a gentle introduction to the key idea of type safety. An optional chapter develops a proof of normalization for the simply typed lambda-calculus using Tait's method. Part 3 addresses the fundamental mechanism of subtyping: it includes a detailed discussion of metatheory and two extended case studies. Part 4 covers recursive types, in both the simple iso-recursive and the tricker equi-recursive formulations. The second of the two chapters in this part develops the metatheory of a system with equi-recursive types and subtyping in the mathematical framework of coinduction. Part 5 takes polymorphism with chapters on ML-style type reconstruction, the more powerful impredicative polymorphism of System \(F\), existential quantification and its connections with abstract data types, and the combination of polymorphism and subtyping in systems with bounded quantification. Part 6 deals with type operators. One chapter covers basic concepts; the next develops System \(F_w\) and its metatheory; the next combines type operators and bounded quantification to yield System \(F_w\); the final chapter is a closing case study. The treatment of each language feature discussed in the book follows a common pattern. Motivating examples are first; the formal definitions; then proofs of basic properties such as type safety; the (usually in a separate chapter) a deeper investigation of metatheory, leading to typechecking algorithms and their proofs of soundness, completeness, and termination; and finally (again in a separate chapter) the concrete realization of these algorithms as an Ocalm (Objective Caml) program. An important source of examples throughout the book is the analysis and design of features for object-oriented programming. Four case study chapters develop different approaches in detail -- a simple model of conventional imperative objects and classes, a core calculus based on Java, a more refined account of imperative objects using bounded quantification, and a treatment of objects and classes in the purely functional setting.
- Amalgamating sessions and methods in object-oriented languages with generics
- HasCasl: integrated higher-order specification and program development
- A rewriting logic approach to operational semantics
- Featherweight Java with dynamic and static overloading
- Objects and session types
- Recasting ML\(^{\text F}\)
- Multiparty session types, beyond duality
- Composition-nominative logics as institutions
- Type soundness for path polymorphism
- Towards proving type safety of \(\mathrm{C}^{\#}\)
- A type system for counting instances of software components
- Amalgamation in the semantics of CASL
- On the complexity of deciding typability in the relational algebra
- Encoding types in ML-like languages
- Parametric parameter passing \(\lambda\)-calculus
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
- Composition and decomposition of multiparty sessions
- Verifying pointer and string analyses with region type systems
- Enhanced type inference for binding-time analysis
- From specification to testing: semantics engineering for Lua 5.2
- Polymorphic lambda calculus with context-free session types
- Session-based concurrency, declaratively
- Gradual typing using union typing with records
- Nonlinear pattern matching in rule-based modeling languages
- A program logic for fresh name generation
- Abstraction and subsumption in modular verification of C programs
- Functional sets with typed symbols: Mixed zonotopes and polynotopes for hybrid nonlinear reachability and filtering
- Region analysis for deductive verification of C programs
- Verified software units
- On quantified linear implications
- Global types with internal delegation
- Reversible sessions with flexible choices
- QPCF: higher-order languages and quantum circuits
- Observational program calculi and the correctness of translations
- Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus
- Minimal type inference for linked data consumers
- Data-driven adaptation for smart sessions
- On the value of variables
- Model approach to grammatical evolution: theory and case study
- A graph-based generic type system for object-oriented programs
- Precise subtyping for synchronous multiparty sessions
- A reduction semantics for direct-style asynchronous observables
- Typed path polymorphism
- Formalising Java RMI with explicit code mobility
- Domain-theoretical models of parametric polymorphism
- Translating higher-order clauses to first-order clauses
- Semantic essence of AsmL
- MOMI: a calculus for mobile mixins
- Subtyping for session types in the pi calculus
- Comparing type systems for deadlock freedom
- Fairness and communication-based semantics for session-typed languages
- Reasoning in Abella about structural operational semantics specifications
- Categories of timed stochastic relations
- Practical foundations for programming languages
- Implicit propagation in structural operational semantics
- A gentle introduction to multiparty asynchronous session types
- A type theory for robust failure handling in distributed systems
- A calculus of global interaction based on session types
- A parametric calculus for mobile open code
- Rule-based operational semantics for an imperative language
- A rewriting logic approach to operational semantics (extended abstract)
- An institutional theory for \#-components
- Homotopy type theory and Voevodsky's univalent foundations
- Environment classifiers
- Bigraphs and transitions
- The M-calculus: a higher-order distributed process calculus
- A generic approach to the static analysis of concurrent programs with procedures
- Discovering affine equalities using random interpretation
- Bitwidth aware global register allocation
- Folklore confirmed
- New results on the computability and complexity of points-to analysis
- Incremental algorithms for dispatching in dynamically typed languages
- From control effects to typed continuation passing
- Coercive subtyping for the calculus of constructions (extended abstract)
- A type theory for memory allocation and data layout
- Static prediction of heap space usage for first-order functional programs
- Ownership types for object encapsulation
- Guarded recursive datatype constructors
- A type system for higher-order modules
- Pure patterns type systems
- A coordination language for databases
- The essence of functional programming on semantic data
- \textsc{qPCF}: a language for quantum circuit computations
- Typing local control and state using flow analysis
- A New Method for Dependent Parsing
- MikiBeta : A General GUI Library for Visualizing Proof Trees
- A language for biochemical systems: design and formal specification
- The rewriting logic semantics project: a progress report
- Full abstraction in a subtyped pi-calculus with linear types
- PiStache: implementing -calculus in Scala
- A formal language for cyclic operads
- Self-adaptation and secure information flow in multiparty communications
- Combining model checking and data-flow analysis
- New
- A realizability interpretation for intersection and union types
- Unified syntax with iso-types
- The HOL-Omega Logic
- Types in programming languages, between modelling, abstraction, and correctness (extended abstract)
- Subtyping Supports Safe Session Substitution
- The recursive union of some gradual types
This page was built for publication: Types and programing languages
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2778806)
