1. Home
    2. Journals
    3. Sadhana
    4. Volume 34
    5. Issue 1

    • Fulltext

       

        Click here to view fulltext PDF


      Permanent link:
      https://www.ias.ac.in/article/fulltext/sadh/034/01/0071-0144

    • Keywords

       

      Interactive theorem provers; calculus of inductive constructions; Matita; Kernel.

    • Abstract

       

      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.

    • Author Affiliations

       

      A Asperti1 W Ricciotti1 C Sacerdoti Coen1 E Tassi1

      1. Department of Computer Science, University of Bologna, Italy

    • Dates

       
      Published
      February 2009

  • Sadhana | News

    • Editorial Note on Continuous Article Publication

      Posted on July 25, 2019

      Click here for Editorial Note on CAP Mode

© 2021-2022 Indian Academy of Sciences, Bengaluru.

Contact | Site index