Open Daily: 10am - 10pm | Alley door pickup 10am - 7pm 3038 Hennepin Ave Minneapolis, MN
612-822-4611

  • Open Daily: 10am - 10pm
    Alley-side Pickup: 10am - 7pm

    3038 Hennepin Ave Minneapolis, MN
    612-822-4611

Open Daily: 10am - 10pm | Alley-side Pickup: 10am - 7pm
3038 Hennepin Ave Minneapolis, MN
612-822-4611
Proof Assistants and Their Applications in Mathematics and Computer Science

Proof Assistants and Their Applications in Mathematics and Computer Science

Blanchette, Jasmin
Mahboubi, Assia

Hardcover

Series: Computer Science Foundations and Applied Logic

FictionGeneral ComputersGeneral Mathematics

PREORDER - Expected ship date January 9, 2027

ISBN10: 3031851897
ISBN13: 9783031851896
Publisher: Springer
Published: Jan 9 2027
Pages: 390
Language: English
Proof assistants are computer programs that help users formally describe mathematical statements and proofs, making them amenable to mechanical checking. Today they are used to verify operating systems, compilers, and cryptographic protocols, as well as landmark results in mathematics such as the Feit-Thompson theorem or the Kepler conjecture. Contemporary proof assistants rely on a sophisticated interaction between theoretical investigations in metamathematics and the efficient implementation of a portfolio of algorithms, without which these systems would not usable on a large scale. During the last decade, the use of proof assistants has grown steadily, and they are now at the same time a research topic in its own right and a tool for researchers in other domains. Yet no reference book is available today that covers the entire domain. This book is an introduction and reference for the various topics related to the underlying logical formalisms, architectures, and applications.

Also from

Blanchette, Jasmin

View All

Also in

General Computers

View All