Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions
Explore this paper's citation graph
- Type
- preprint
- Published
- 2010-12-01
- Cited by
- 1,782
- References
- 0
- OpenAlex
- https://openalex.org/W1508641834
- Semantic Scholar
- https://api.semanticscholar.org/CorpusID:118062581
Keywords
Calculus (dental), Development (topology), Inductive method, Computer science, Programming language
References
No references recorded for this paper.
Cited by
- Inductive representation, proofs and refinement of pointer structures
- Verification based on unfoldings of Petri nets with read arcs. (Vérification à l'aide de dépliages de réseaux de Petri étendus avec des arcs de lecture)
- Study of the Benefits of Using Deductive Formal Methods for Secure Developments. (Etude de l'apport des méthodes formelles déductives pour les développements de sécurité)
- Types and verification for infinite state systems
- Certifying homological algorithms to study biomedical images
- Towards an Interlinked Semantic Wiki Farm
- Common Grounds for Modelling Mathematics in Educational Software.
- Coinductive Techniques in Infinitary Lambda-Calculus
- Abstraction d'horloges dans les systemes synchrones flot de donnees
- Développement prouvé de composants formels pour un générateur de code embarqué critique pré-qualifié. (Proved Development of Formal Components for a Pre-Qualified Critical Embedded Code Generator)
- Especicaci on Formal del Modelo RBAC en el C alculo de Construcciones Inductivas
- Language-based Enforcement of User-defined Security Policies (As Applied to Multi-tier Web Programs)
- Automatisation de la Certification Formelle de Systèmes Critiques par Instrumentation d'Interpréteurs Abstraits. (Automatic and formal certification of critical systems by instrumentation of abstract interpreters)
- Initial Semantics for higher-order typed syntax
- Formal Proof—The Four- Color Theorem
- Contributions to the Formal Verification of Arithmetic Algorithms. (Contributions à la vérification formelle d'algorithmes arithmétiques)
- Mise en œuvre de techniques de démonstration automatique pour la vérification formelle des NoCs
- Congruence closure with ACI function symbols
- Verification Condition Generation with the Dijkstra State Monad
- Invariant discovery and refinement plans for formal modelling in Event-B
Related papers
- Primärzerlegung in Steinschen Algebren
- Über unirationale Scharen auf algebraischen Mannigfaltigkeiten
- Algebraic Set Operations, Multifunctions, and Indefinite Integrals
- On Almost α(Λ, sp)-continuous Multifunctions
- Produkttreue Klassen universeller Algebren
- Approximation of fixed points of multifunctions in partial metric spaces
- The World of Jagdish N. Srivastava
- Hardy spaces of analytic multifunctions.
- The equivalence of uninorms induced by the U-partial order
- Surjectivity of multifunctions under generalized differentiability assumptions