A compact kernel for the calculus of inductive constructions
A Asperti W Ricciotti C Sacerdoti Coen E Tassi
Click here to view fulltext PDF
Permanent link:
https://www.ias.ac.in/article/fulltext/sadh/034/01/0071-0144
The paper describes the new kernel for the Calculus of Inductive Constructions (CIC) implemented inside the Matita Interactive Theorem Prover. The design of the new kernel has been completely revisited since the first release, resulting in a remarkably compact implementation of about 2300 lines of OCaml code. The work is meant for people interested in implementation aspects of Interactive Provers, and is not self contained. In particular, it requires good acquaintance with Type Theory and functional programming languages.
A Asperti1 W Ricciotti1 C Sacerdoti Coen1 E Tassi1
Volume 45, 2020
All articles
Continuous Article Publishing mode
Click here for Editorial Note on CAP Mode
© 2021-2022 Indian Academy of Sciences, Bengaluru.