Một cuốn sổ tay cho phần mềm Coq để viết và kiểm tra các bằng chứng toán học, với trọng tâm kỹ thuật thực tế. Công nghệ xác minh chương trình cơ giới hóa có thể đóng vai trò hỗ trợ trong nhiều loại dự án nghiên cứu về khoa học máy tính và các công cụ liên quan để kiểm tra hiệu đính chính thức đang được áp dụng ngày càng tăng trong toán học và kỹ thuật. Cuốn sách này giới thiệu về phần mềm Coq để viết và kiểm tra các bằng chứng toán học. Nó tập trung vào kỹ thuật thực tế xuyên suốt, nhấn mạnh các kỹ thuật sẽ giúp người dùng xây dựng, hiểu và duy trì sự phát triển Coq lớn và giảm thiểu chi phí thay đổi mã theo thời gian. Hai chủ đề, hiếm khi được thảo luận ở nơi khác, được đề cập chi tiết: lập trình gõ phụ thuộc hiệu quả (sử dụng hiệu quả một tính năng ở trung tâm của hệ thống Coq) và xây dựng các chiến thuật chứng minh miền cụ thể. Hầu hết mọi chủ đề được đề cập cũng có liên quan đến định lý máy tính tương tác chứng minh nói chung, không chỉ xác minh chương trình, được thể hiện thông qua các ví dụ về các chương trình đã được xác minh được áp dụng trong nhiều loại chính thức hóa khác nhau. Cuốn sách phát triển một phong cách chứng minh tự động độc đáo và áp dụng nó xuyên suốt; ngay cả những người dùng Coq có kinh nghiệm cũng có thể được hưởng lợi từ việc đọc về các khái niệm Coq cơ bản từ quan điểm mới lạ này. Cuốn sách cũng cung cấp một thư viện các chiến thuật, hoặc các chương trình tìm bằng chứng, được thiết kế để sử dụng với các ví dụ trong cuốn sách. Người đọc sẽ có được các kỹ năng cần thiết để thực hiện lại các chiến thuật này trong các cài đặt khác vào cuối cuốn sách. Tất cả các mã xuất hiện trong cuốn sách đều có sẵn miễn phí trực tuyến.

Abstract:

A handbook to the Coq software for writing and checking mathematical proofs, with a practical engineering focus. The technology of mechanized program verification can play a supporting role in many kinds of research projects in computer science, and related tools for formal proof-checking are seeing increasing adoption in mathematics and engineering. This book provides an introduction to the Coq software for writing and checking mathematical proofs. It takes a practical engineering focus throughout, emphasizing techniques that will help users to build, understand, and maintain large Coq developments and minimize the cost of code change over time. Two topics, rarely discussed elsewhere, are covered in detail: effective dependently typed programming (making productive use of a feature at the heart of the Coq system) and construction of domain-specific proof tactics. Almost every subject covered is also relevant to interactive computer theorem proving in general, not just program verification, demonstrated through examples of verified programs applied in many different sorts of formalizations. The book develops a unique automated proof style and applies it throughout; even experienced Coq users may benefit from reading about basic Coq concepts from this novel perspective. The book also offers a library of tactics, or programs that find proofs, designed for use with examples in the book. Readers will acquire the necessary skills to reimplement these tactics in other settings by the end of the book. All of the code appearing in the book is freely available online.

Ngôn ngữ:	En
Tác giả:	Chlipala, Adam
Thông tin nhan đề:	Certified Programming with Dependent Types
Nhà xuất bản:	The MIT Press
Loại hình:	Tài nguyên giáo dục mở / Bộ sưu tập: Công nghệ thông tin
Bản quyền:	http://creativecommons.org/licenses/by-nc-nd/4.0
Nguồn gốc:	https://directory.doabooks.org/handle/20.500.12854/78523
Mô tả vật lý:	440p.
Năm xuất bản:	2013