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)

• Herbrand constructivization for automated intuitionistic theorem proving
• Extending Sledgehammer with SMT solvers
• From signatures to monads in \textsf{UniMath}
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• A graphical user interface for formal proofs in geometry
• A web-based toolkit for mathematical word processing applications with semantics
• Functional and Logic Programming
• Automating Induction with an SMT Solver
• Lem: reusable engineering of real-world semantics
• Compositional CompCert
• MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
• Certification of bounds on expressions involving rounded operators
• The power of parameterization in coinductive proof
• Formalizing the LLVM intermediate representation for verified program transformations
• Fiat: deductive synthesis of abstract data types in a proof assistant
• Chapar: certified causally consistent distributed key-value stores
• Mechanical Verification of a Constructive Proof for FLP
• A synthesis of the procedural and declarative styles of interactive theorem proving
• A Brief Overview of Mizar
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Separation Logic for Small-Step cminor
• Ivor, a Proof Engine
• Modeling Permutations in Coq for Coccinelle
• Automath and Pure Type Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Ott: Effective tool support for the working semanticist
• Title not available (Why is that?)
• AURA
• CompCertTSO
• Program verification through characteristic formulae
• Mathematical Knowledge Management
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Formal certification of code-based cryptographic proofs
• Title not available (Why is that?)
• HOL Light QE
• Title not available (Why is that?)
• A certified framework for compiling and executing garbage-collected languages
• JCML: A specification language for the runtime verification of Java card programs
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}
• Innovations in computational type theory using Nuprl
• SAD as a mathematical assistant -- how should we go from here to there?
• HasCasl: integrated higher-order specification and program development
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• CompCertS: a memory-aware verified C compiler using pointer as integer semantics
• FoCaLiZe and Dedukti to the rescue for proof interoperability
• Proviola: a tool for proof re-animation
• Saoithín: a theorem prover for UTP
• Sawja: static analysis workshop for Java
• The Matita interactive theorem prover
• Automatic proof and disproof in Isabelle/HOL
• A coherent logic based geometry theorem prover capable of producing formal and readable proofs
• A first step in the design of a formally verified constraint-based testing tool: FocalTest
• ML4PG in computer algebra verification
• Overview of the Mathemagix type system
• Ott, effective tool support for the working semanticist
• The relation tool in GeoGebra 5
• Mizar: state-of-the-art and beyond
• Termination of Isabelle functions via termination of rewriting
• The logic of \(U\cdot(TP)^{2}\)
• Hammer for Coq: automation for dependent type theory
• VST-Floyd: a separation logic tool to verify correctness of C programs
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• A new implementation of Automath
• Communicating formal proofs: the case of Flyspeck
• Bellerophon: tactical theorem proving for hybrid systems
• A trustworthy proof checker
• NLCertify: a tool for formal nonlinear optimization
• Formalizing the SAFECode type system
• ReCaml: execution state as the cornerstone of reconfigurations
• VeriML: typed computation of logical terms inside a language with effects
• Ynot: dependent types for imperative programs
• Mtac: a monad for typed tactic programming in Coq
• Foundational property-based testing
• ROSCoq: robots powered by constructive reals
• ModuRes: a Coq library for modular reasoning about concurrent higher-order imperative programming languages
• Theorema 2.0: computer-assisted natural-style mathematics
• NetKAT -- a formal system for the verification of networks
• A program logic for verifying secure routing protocols
• CAMPARY: CUDA multiple precision arithmetic library and applications
• Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials
• ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti
• Towards certified meta-programming with typed Template-Coq
• Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture
• SEPIA: search for proofs using inferred automata
• A verified compiler for probability density functions
• Formalizing the Edmonds-Karp algorithm
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
• Friends with benefits. Implementing corecursion in foundational proof assistants
• Coquelicot: a user-friendly library of real analysis for Coq
• TacticToe: learning to reason with HOL4 tactics
• RDA: a Coq library to reason about randomised distributed algorithms in the message passing model
• A linear algorithm for brick Wang tiling

This page was built for software: Coq