Lambda Calculus with Types

Lambda Calculus with Types

This handbook with exercises reveals in formalisms, hitherto mainly used for hardware and

software design and verification, unexpected mathematical beauty.

The lambda calculus forms a prototype universal programming language, which in its

untyped version is related to Lisp, and was treated in the first author’s classic The Lambda

Calculus (1984). The formalism has since been extended with types and used in functional

programming (Haskell, Clean) and proof assistants (Coq, Isabelle, HOL), used in designing

and verifying IT products and mathematical proofs.

at Radboud University, Nijmegen, The Netherlands.

WIL DEKKERS is an Associate Professor in the Institute of Information and Computing

Sciences at Radboud University, Nijmegen, The Netherlands.

RICHARD STATMAN is a Professor of Mathematics at Carnegie Mellon University, Pittsburgh,

USA.

PERSPECTIVES IN LOGIC

The Perspectives in Logic series publishes substantial, high-quality books whose central

theme lies in any area or aspect of logic. Books that present new material not now available

in book form are particularly welcome. The series ranges from introductory texts suitable for

beginning graduate courses to specialized monographs at the frontiers of research. Each book

Thomas Scanlon, Managing Editor

Department of Mathematics, University of California Berkeley

Editorial Board:

Michael Benedikt

Department of Computing Science, University of Oxford

Steven A. Cook

Computer Science Department, University of Toronto

Michael Glanzberg

Department of Philosophy, University of California Davis

Antonio Montalban

Richard A. Shore

Department of Mathematics, Cornell University

For more information, see www.aslonline.org/books_perspectives.html

CAMBRIDGE UNIVERSITY PRESS

Cambridge, New York, Melbourne, Madrid, Cape Town,

Singapore, São Paulo, Delhi, Mexico City

Cambridge University Press

The Edinburgh Building, Cambridge CB2 8RU, UK

Published in the United States of America by Cambridge University Press, New York

permission of Cambridge University Press.

Printed and bound in the United Kingdom by the MPG Books Group

A catalogue record for this publication is available from the British Library

ISBN 978-0-521-766-142 Hardback

Cambridge University Press has no responsibility for the persistence or accuracy of URLs for external

or third-party internet websites referred to in this publication, and does not guarantee that any content

on such websites is, or will remain, accurate or appropriate.