Gilles Dowek

Jean-Jacques Lévy

The design and implementation of programming languages, from Fortran and Cobol to Caml and Java, has been one of the key developments in the management of ever more complex computerized systems. Introduction to the Theory of Programming Languages gives the reader the means to discover the tools to think, design, and implement these languages. It proposes a unified vision of the different formalisms that permit definition of a programming language: small steps operational semantics, big steps operational semantics, and denotational semantics, emphasising that all seek to define a relation between three objects: a program, an input value, and an output value. These formalisms are illustrated by presenting the semantics of some typical features of programming languages: functions, recursivity, assignments, records, objects, ... showing that the study of programming languages does not consist of studying languages one after another, but is organized around the features that are present in these various languages. The study of these features leads to the development of evaluators, interpreters and compilers, and also type inference algorithms, for small languages.

Introduction to the Theory of Programming Languages

Logic is a branch of philosophy, mathematics and computer science. It studies the required methods to determine whether a statement is true, such as reasoning and computation. Proofs and Algorithms: Introduction to Logic and Computability is an introduction to the fundamental concepts of contemporary logic - those of a proof, a computable function, a model and a set. It presents a series of results, both positive and negative, - Church's undecidability theorem, Gödel’s incompleteness theorem, the theorem asserting the semi-decidability of provability - that have profoundly changed our vision of reasoning, computation, and finally truth itself. Designed for undergraduate students, this book presents all that philosophers, mathematicians and computer scientists should know about logic.

An Introduction to Logic and Computability

Proofs and Algorithms

This book constitutes the refereed proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications, RTA 2014, and 12th International Conference on Typed Lambda-Calculi and Applications, TLCA 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 28 revised full papers and 3 short papers presented were carefully reviewed and selected from 87 submissions. The papers provide research results on all aspects of rewriting and typed lambda calculi, ranging from theoretical and methodological issues to applications in various contexts. They address a wide variety of topics such as algorithmic aspects, implementation, logic, types, semantics, and programming.

Joint International Conferences, RTA and TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings

Rewriting and Typed Lambda Calculi

Yves Bertot

Andre Hirschowitz

Christine Paulin

Laurent Thery

This book constitutes the refereed proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '99, held in Nice, France, in September 1999. The 20 revised full papers presented together with three invited contributions were carefully reviewed and selected from 35 papers submitted. All current aspects of higher order theorem proving, formal verification, and specification are discussed. Among the theorem provers evaluated are COQ, HOL, Isabelle, Isabelle/ZF, and OpenMath.

12th International Conference, TPHOLs'99, Nice, France, September 14-17, 1999, Proceedings

Theorem Proving in Higher Order Logics

Peter Baumgartner

Alessandro Armando

methods, description logics and related logics, sati?ability modulo theory, decidable logics, reasoning about programs, and higher-order logics.

4th International Joint Conference, IJCAR 2008, Sydney, NSW, Australia, August 12-15, 2008, Proceedings

Automated Reasoning

Computation, calculation, algorithms - all have played an important role in mathematical progress from the beginning - but behind the scenes, their contribution was obscured in the enduring mathematical literature. To understand the future of mathematics, this fascinating book returns to its past, tracing the hidden history that follows the thread of computation.

Mathematics Enters a New Age

Computation, Proof, Machine

Serge Abiteboul

Algorithms are probably the most sophisticated tools that people have had at their disposal since the beginnings of human history. They have transformed science, industry, society. They upset the concepts of work, property, government, private life, even humanity. Going easily from one extreme to the other, we rejoice that they make life easier for us, but fear that they will enslave us. To get beyond this vision of good vs evil, this book takes a new look at our time, the age of algorithms. Creations of the human spirit, algorithms are what we made them. And they will be what we want them to be: it's up to us to choose the world we want to live in.

The Age of Algorithms

Algorithms will be what we want them to be: we must choose the world we want to live in.

Gilles Dowek

Books

Your next favorite book is out there