Výsledky vyhledávání - "Calculus of Inductive Constructions"

Compositional pre-processing for automated reasoning in dependent type theory

Autor: Blot, Valentin, Cousineau, Denis, Crance, Enzo, de Prisque, Louise Dubois, Keller, Chantal, Mahboubi, Assia, Vial, Pierre

Publikováno v: CPP 2023-Certified Programs and Proofs
CPP 2023-Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩

International audience; In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected l

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fe662381e483c147d8f9996499b886e3
https://inria.hal.science/hal-03901019v2/document

Zobrazit plný text záznamu

Bidirectional Typing for the Calculus of Inductive Constructions

Autor: Lennon-Bertrand, Meven

Publikováno v: Autre [cs.OH]. Nantes Université, 2022. Français. ⟨NNT : 2022NANU4033⟩

Over their more than 50 years of existence, proof assistants have established themselves as tools guaranteeing high trust levels in many applications. Yet, due to their increasing complexity, the historical solution of relying on a small, trusted ker

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::b837cb1557f288942e8a0d71e5a4984f
https://theses.hal.science/tel-03848595v2

Zobrazit plný text záznamu

Complete Bidirectional Typing for the Calculus of Inductive Constructions

Autor: Lennon-Bertrand, Meven

Publikováno v: ITP 2021-12th International Conference on Interactive Theorem Proving
ITP 2021-12th International Conference on Interactive Theorem Proving, Jun 2021, Rome, Italy. pp.1-19, ⟨10.4230/LIPIcs.ITP.2021.24⟩
12th International Conference on Interactive Theorem Proving (ITP 2021)
12th International Conference on Interactive Theorem Proving (ITP 2021), Jun 2021, Rome, Italy. pp.24:1--24:19, ⟨10.4230/LIPIcs.ITP.2021.24⟩

This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). The key property of the system is its completeness with respect to the usual undirected one, which has been formally proven in Coq as a part of the M

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::66c8d37b20203d16bb77de8684a075be
http://arxiv.org/abs/2102.06513

Zobrazit plný text záznamu

Hammer for Coq: Automation for Dependent Type Theory

Autor: Łukasz Czajka, Cezary Kaliszyk

Publikováno v: Journal of Automated Reasoning

Hammers provide most powerful general purpose automation for proof assistants based on HOL and set theory today. Despite the gaining popularity of the more advanced versions of type theory, such as those based on the Calculus of Inductive Constructio

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4686567200bfd81682d74600e52afeae
https://doi.org/10.1007/s10817-018-9458-4

Zobrazit plný text záznamu

Conference

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Formalizing Abstract Computability: Turing Categories in Coq

Autor: Vinogradova, Polina

The concept of a recursive function has been extensively studied using traditional tools of computability theory. However, with the development of category-theoretic methods it has become possible to study recursion in a more general (abstract) sense

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::82acfeea10e99d475ac829314980ac55

Zobrazit plný text záznamu

A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading

Autor: Beta Ziliani, Matthieu Sozeau

Publikováno v: Journal of Functional Programming
Journal of Functional Programming, Cambridge University Press (CUP), 2017, 27, ⟨10.1017/S0956796817000028⟩
Journal of Functional Programming, 2017, 27, ⟨10.1017/S0956796817000028⟩

Unification is a core component of every proof assistant or programming language featuring dependent types. In many cases, it must deal with higher order problems up to conversion. Since unification in such conditions is undecidable, unification algo

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::277f5abf236c5bbc239827cee9b8b9f6
https://doi.org/10.1017/s0956796817000028

Zobrazit plný text záznamu

A compact kernel for the calculus of inductive constructions

Autor: C. Sacerdoti Coen, Andrea Asperti, Enrico Tassi, Wilmer Ricciotti

Publikováno v: Sadhana. 34:71-144

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 remarkab

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8020ac51749fb6d581ff8e727aca63a1
https://doi.org/10.1007/s12046-009-0003-3

Zobrazit plný text záznamu

Introduction to the Calculus of Inductive Constructions

Autor: Paulin-Mohring, Christine

Publikováno v: All about Proofs, Proofs for All
Bruno Woltzenlogel Paleo; David Delahaye. All about Proofs, Proofs for All, 55, College Publications, 2015, Studies in Logic (Mathematical logic and foundations), 978-1-84890-166-7

International audience; This paper gives an introduction to the Calculus of Inductive Constructions, the formalism behind the Coq proof assistant. We present the language and the typing rules, starting with the pure functional part and then introduci

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::b7c0c1c68994d490537c3b18626dc76f
https://hal.inria.fr/hal-01094195

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání