Books On Rocq (16)

The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Rocq Prover.

Separation Logic Foundations is an in-depth introduction to separation logic—a practical approach to modular verification of imperative programs—and how to build program verification tools on top of it.

The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Rocq Prover.

Verified Functional Algorithms shows how a variety of fundamental data structures can be specified and mechanically verified.

The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Rocq Prover.

Logical Foundations is the entry-point to the series. It covers functional programming, basic concepts of logic, computer-assisted theorem proving, and the Rocq Prover.

The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Rocq Prover.

QuickChick: Property-Based Testing in Rocq introduces tools for combining randomized property-based testing with formal specification and proof in the Rocq ecosystem.

《软件基础》系列广泛地介绍了可靠软件的数学基础。

本系列书籍最主要的新颖之处在于，书中的每一处细节都百分之百地形式化且通过了机器验证。每卷书中的所有文本，包括练习，都是一份 Rocq 证明助理的「证明脚本」。

本系列书籍的目标受众包括从高年级本科生到博士以及研究者在内的广大读者。书中并未假定读者有逻辑学或编程语言的背景，不过一定的数学熟练度会很有帮助。

1. 《逻辑基础》为本系列书籍的切入点。它涵盖了函数式编程、逻辑的基本概念、计算机辅助定理证明以及 Rocq 证明助理。
2. 《编程语言基础》考察了编程语言理论，包括操作语义、霍尔逻辑以及静态类型系统。
3. 《函数式算法验证》展示了如何对各种基础数据结构进行机器验证。
4. 《QuickChick：用 Rocq 进行基于性质的测试》介绍了将随机化基于性质的测试与 Rocq 生态系统中的形式化规范和证明相结合的工具和技术。

The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Rocq Prover.

Programming Language Foundations surveys the theory of programming languages, including operational semantics, Hoare logic, and static type systems.

The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Rocq Prover.

Verifiable C is an extended hands-on tutorial on specifying and verifying real-world C programs using the Princeton Verified Software Toolchain.

Mathematical Components is the name of a library of formalized mathematics for the Rocq Prover. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order Theorem.

This book aims at providing an introducing to the design patterns used throughout this library, so as to ease its use for other projects. While there are several books around covering the usage of the Rocq Prover and the theory it is based on, the Mathematical Components library uses a few design patterns that differ from the methodology proposed in other sources. As a consequence, this book provides a slightly non-standard presentation of Rocq, putting upfront the formalization choices and the proof style that are the pillars of the library.

This books targets two natures of audience. On the one hand newcomers, in particular beginners with background in mathematics rather than computer science, should find a soft introduction to the programming language of the Rocq Prover, Gallina, and to the SSReflect proof language used in the Mathematical Components library. On the other hand, accustomed Rocq users will find a substantial account of the formalization style that made the Mathematical Components library possible.

These lecture notes are the result of the author's personal experience of learning how to structure formal reasoning using the Rocq Prover and employ Rocq in large-scale research projects. The present manuscript offers a brief and practically-oriented introduction to the basic concepts of mechanized reasoning and interactive theorem proving.

The primary audience of the manuscript are the readers with expertise in software development and programming and knowledge of discrete mathematic disciplines on the level of an undergraduate university program. The high-level goal of the course is, therefore, to demonstrate how much the rigorous mathematical reasoning and development of robust and intellectually manageable programs have in common, and how understanding of common programming language concepts provides a solid background for building mathematical abstractions and proving theorems formally. The low-level goal of this course is to provide an overview of the Rocq Prover, taken in its both incarnations: as an expressive functional programming language with dependent types and as a proof assistant providing support for mechanized interactive theorem proving.

By aiming these two goals, this manuscript is, thus, intended to provide a demonstration how the concepts familiar from the mainstream programming languages and serving as parts of good programming practices can provide illuminating insights about the nature of reasoning in Rocq's logical foundations and make it possible to reduce the burden of mechanical theorem proving. These insights will eventually give the reader a freedom to focus solely on the essential part of the formal development instead of fighting with the proof assistant in futile attempts to encode the "obvious" mathematical intuition.

Modeling and Proving in Computational Type Theory (MPCTT) is a textbook covering topics in computational logic using the Rocq Prover. The book provides a foundational theory and a programming language for interactively constructing computational models with machine-checked proofs. As common with programming languages, the book covers foundations, case studies, and practical programming in an interleaved fashion.

Floating-point arithmetic is ubiquitous in modern computing, as it is the tool of choice to approximate real numbers. Due to its limited range and precision, its use can become quite involved and potentially lead to numerous failures. One way to greatly increase confidence in floating-point software is by computer-assisted verification of its correctness proofs.

This book provides a comprehensive view of how to formally specify and verify tricky floating-point algorithms with the Coq proof assistant. It describes the Flocq formalization of floating-point arithmetic and some methods to automate theorem proofs. It then presents the specification and verification of various algorithms, from error-free transformations to a numerical scheme for a partial differential equation. The examples cover not only mathematical algorithms but also C programs as well as issues related to compilation.

** Certified Programming with Dependent Types (CPDT)** is a hands-on guide to advanced programming and proving using the Rocq Prover.

The book focuses on leveraging Roqc’s dependent type system to write certified programs, where correctness is formally verified alongside implementation. It introduces key concepts such as inductive types, type theory, proof automation, and advanced tactics, providing a blend of theoretical foundations and practical examples. CPDT is particularly known for its focus on proof engineering and building large-scale verified systems efficiently. Aimed at readers with some prior exposure to Rocq, it serves as an invaluable resource for those looking to master the interplay between programming and formal verification.

Formal Reasoning About Programs (FRAP) is a book that provides a general introduction to formal logical reasoning about the correctness of programs and to using Rocq for this purpose. The main narrative of FRAP presents standard program-proof ideas, without rigorous proofs. Matching Rocq code then show how to make it rigorous. Interleaved with that narrative, there are also other lectures' worth of material, for building up more practical background on Rocq itself.

Separation Logic is the twenty-first-century variant of Hoare Logic that permits verification of pointer-manipulating programs. This book covers practical and theoretical aspects of Separation Logic at a level accessible to beginning graduate students interested in software verification. On the practical side it offers an introduction to verification in Hoare and Separation logics, simple case studies for toy languages, and the Verifiable C program logic for the C programming language. On the theoretical side it presents separation algebras as models of separation logics; step-indexed models of higher-order logical features for higher-order programs; indirection theory for constructing step-indexed separation algebras; tree-shares as models for shared ownership; and the semantic construction (and soundness proof) of Verifiable C. In addition, the book covers several aspects of the CompCert verified C compiler, and its connection to foundationally verified software analysis tools. All constructions and proofs are made rigorous and accessible in the Coq developments of the open-source Verified Software Toolchain.

Le Coq'Art (nom complet en anglais Coq'Art: The Calculus of Inductive Constructions) est le premier livre a avoir été écrit sur le Prouveur Rocq (à l'époque appelé Coq) et sa théorie sous-jacente, le Calcul des Constructions Inductives (CIC). La version française de ce livre est disponible en ligne gratuitement. Ce livre fournit un guide complet de la preuve interactive, combinant théorie et applications pratiques. Il couvre des concepts clés tels que les types inductifs, les fonctions récursives et la construction de preuves, tout en offrant de nombreux exemples et études de cas, y compris la formalisation d'algorithmes et de preuves mathématiques. Coq'Art sert à la fois d'introduction pour les débutants et de référence pour les experts, en faisant une ressource essentielle pour quiconque travaille avec Rocq ou explore les méthodes formelles.

Coq'Art: The Calculus of Inductive Constructions is a foundational book that introduces readers to the Rocq Prover and its underlying formal system, the Calculus of Inductive Constructions (CIC). The book provides a comprehensive guide to interactive theorem proving, combining theory with practical applications. It covers key concepts such as inductive types, recursive functions, and proof construction, while offering numerous examples and case studies, including the formalization of algorithms and mathematical proofs. Coq'Art serves as both an introduction for beginners and a reference for experts, making it an essential resource for anyone working with Rocq or exploring formal methods.