Applied Semantics

1. Front Matter

   Pages I-VIII

   PDF

2. An Introduction to Dependent Type Theory

   • Gilles Barthe, Thierry Coquand

   Pages 1-41

3. Monads and Effects

   • Nick Benton, John Hughes, Eugenio Moggi

   Pages 42-122

4. Abstract Machines, Control, and Sequents

   • Pierre-Louis Curien

   Pages 123-136

5. Normalization and Partial Evaluation

   • Peter Dybjer, Andrzej Filinski

   Pages 137-192

6. Computing with Real Numbers

   • Abbas Edalat, Reinhold Heckmann

   Pages 193-267

7. The Join Calculus: A Language for Distributed Mobile Programming

   • Cédric Fournet, Georges Gonthier

   Pages 268-332

8. An Introduction to Functional Nets

   • Martin Odersky

   Pages 333-377

9. Operational Semantics and Program Equivalence

   • Andrew M. Pitts

   Pages 378-412

10. Using, Understanding, and Unraveling the OCaml Language From Practice to Theory and Vice Versa

    • Didier Rémy

    Pages 413-536

11. Back Matter

    Pages 537-537

    PDF

This book is based on material presented at the international summer school on Applied Semantics that took place in Caminha, Portugal, in September 2000. We aim to present some recent developments in programming language research, both in semantic theory and in implementation, in a series of graduate-level lectures. The school was sponsored by the ESPRIT Working Group 26142 on Applied Semantics(APPSEM),whichoperatedbetweenApril1998andMarch2002.The purpose of this working group was to bring together leading reseachers, both in semantic theory and in implementation, with the speci?c aim of improving the communication between theoreticians and practitioners. TheactivitiesofAPPSEMwerestructuredintonineinterdisciplinarythemes: A: Semantics for object-oriented programming B: Program structuring C: Integration of functional languages and proof assistants D: Veri?cation methods E: Automatic program transformation F: Games, sequentiality, and abstract machines G: Types and type inference in programming H: Semantics-based optimization I: Domain theory and real number computation These themes were identi?ed as promising for pro?table interaction between semantic theory and practice, and were chosen to contribute to the following general topics: – description of existing programming language features; – design of new programming language features; – implementation and analysis of programming languages; – transformation and generation of programs; – veri?cation of programs. The chapters in this volume give examples of recent developments covering a broad range of topics of interest to APPSEM.

• Program Semantics
• Program Structuring
• Program Verification
• Programming Calculi
• Programming Language Design
• Programming Language Implementation
• Programming Languages
• Programming Theory
• Type Theory
• programming
• programming language
• semantic
• semantics
• verification

• Projet Lemme, INRIA Sophia-Antipolis, Sophia Antipolis Cedex, France

  Gilles Barthe

• Department of Computing Science, Chalmers University of Technology, Göteborg, Sweden

  Peter Dybjer

• Departamento de Matemática, Universidade do Minho, Braga, Portugal

  Luís Pinto

• Departamento de Informática, Universidade do Minho, Braga, Portugal

  João Saraiva

Policies and ethics