Interactive Theorem Proving and Program Development. Coq'Art

Bertot, Y., & Castéran, P. (2004). Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer.

Type

Book

Intellectual base

Review or monograph

Year

2004

DOI

10.1007/978-3-662-07964-5

ISBN

9783642058806

Link

https://doi.org/10.1007/978-3-662-07964-5

Cited from

philosophy

Cited by

1 citation across 1 artifact.

Each citation links to the sentence it supports in the citing article.

Primes

• Deductive Reasoning
  • Higher-order deduction — proof of program correctness: Interactive theorem provers like Coq

    This sourceCoq embeds programming within a logic based on the calculus of inductive constructions; a program proof is a deductive derivation. WebSearch confirmed author, title, year, publisher, and CIC subject.

Verification

This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.

Registry ID ref:db35fa6159a1 · see in the full table