Bertot, Yves
Interactive theorem proving and program development : Coq'Art - the calculus of inductive constructions
- Berlin Springer 2004
- xxv, 469 p. 25 cm.
9783540208549
Logic
Mathematical
Data Type
Automation
Module System
Data Structure
Search Pattern
004.015113 / BER