Coq

swMATH161WikidataQ1131652 ScholiaQ1131652MaRDI QIDQ12929FDOQ12929

Author name not available (Why is that?)

Described by source

• Formalizing generalized maps in Coq
• 30 years of research and development around Coq
• Unnamed Publication

Cited In (only showing first 100 items - show all)

• CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications
• Dependent Types at Work
• The future of logic: foundation-independence
• Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
• Maintaining a library of formal mathematics
• Metamath Zero: designing a theorem prover prover
• On a machine-checked proof for fraction arithmetic over a GCD domain
• A scalable module system
• The \textsc{MetaCoq} project
• Characteristic formulae for the verification of imperative programs
• A Formally-Verified Alias Analysis
• Representing model theory in a type-theoretical logical framework
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Category theory, logic and formal linguistics: some connections, old and new
• Dependent ML An approach to practical programming with dependent types
• A constructive approach to sequential Nash equilibria
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Four decades of {\textsc{Mizar}}. Foreword
• Improving legibility of formal proofs based on the close reference principle is NP-hard
• Reconsidering pairs and functions as sets
• Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
• Completeness and decidability results for CTL in constructive type theory
• Interactive theorem proving. Preface of the special issue
• Mechanizing a process algebra for network protocols
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Verified abstract interpretation techniques for disassembling low-level self-modifying code
• Nominal logic, a first order theory of names and binding
• Some lambda calculus and type theory formalized
• Inductive families
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Set theory for verification. I: From foundations to functions
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• A constructive algebraic hierarchy in Coq.
• A rewriting approach to satisfiability procedures.
• A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
• A mechanically verified theory of contracts
• Evaluating general purpose automated theorem proving systems
• Flexary connectives in Mizar
• A new look at generalized rewriting in type theory
• Sets in Coq, Coq in Sets
• An introduction to small scale reflection in Coq
• Beyond provable security verifiable IND-CCA security of OAEP
• Correct code containing containers
• Point-free, set-free concrete linear algebra
• A verified runtime for a verified theorem prover
• Dependencies in formal mathematics: applications and extraction for Coq and Mizar
• Challenges and experiences in managing large-scale proofs
• A refinement-based approach to computational algebra in Coq
• Secure distributed programming with value-dependent types
• Secure distributed programming with value-dependent types
• Certified Reasoning with Infinity
• TPS: A theorem-proving system for classical type theory
• Injective types in univalent mathematics
• Inductive and coinductive components of corecursive functions in Coq
• Isabelle's metalogic: formalization and proof checker
• A formalization and proof checker for Isabelle's metalogic
• A brief account of runtime verification
• Types for Proofs and Programs
• Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings
• Trace-Based Coinductive Operational Semantics for While
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• Psi-calculi in Isabelle
• Formalization of Bernstein polynomials and applications to global optimization
• Locales: a module system for mathematical theories
• Premise selection for mathematics by corpus analysis and kernel methods
• Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22--25, 2005. Proceedings.
• Formalization of real analysis: a survey of proof assistants and libraries
• A two-level logic approach to reasoning about computations
• A proof strategy language and proof script generation for Isabelle/HOL
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• SMT proof checking using a logical framework
• Translating higher-order clauses to first-order clauses
• Crafting a Proof Assistant
• Extracting a data flow analyser in constructive logic
• Mechanized semantics for the clight subset of the C language
• Two-Way Automata in Coq
• GeoThms -- a web system for Euclidean constructive geometry
• Proof-producing translation of higher-order logic into pure and stateful ML
• Two-level hybrid: a system for reasoning using higher-order abstract syntax
• Completeness and Decidability Results for CTL in Coq
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• Towards a Formally Verified Proof Assistant
• Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
• Improving legibility of natural deduction proofs is not trivial
• More SPASS with Isabelle
• Effective interactive proofs for higher-order imperative programs
• High-level separation logic for low-level code
• Programming with binders and indexed data-types
• On the Generation of Positivstellensatz Witnesses in Degenerate Cases
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Certified Static Analysis by Abstract Interpretation
• A Computational Approach to Pocklington Certificates in Type Theory
• Implementing the cylindrical algebraic decomposition within the Coq system
• A Declarative Language for the Coq Proof Assistant
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL

This page was built for software: Coq