Coq
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
- Mathematical Knowledge Management
- A bi-directional refinement algorithm for the calculus of (co)inductive constructions
- Unifying Sets and Programs via Dependent Types
- Proof assistant decision procedures for formalizing origami
- Comprehending Isabelle/HOL’s Consistency
- scientific article; zbMATH DE number 1303350 (Why is no real title available?)
- A promising semantics for relaxed-memory concurrency
- Interactive proofs in higher-order concurrent separation logic
- Rigorous floating-point mixed-precision tuning
- Non-constructive complex analysis in Coq
- Intuitionistic completeness of first-order logic
- The Picard Algorithm for Ordinary Differential Equations in Coq
- Computation on abstract data types. The extensional approach, with an application to streams
- Intelligent computer mathematics. 9th international conference, AISC 2008, 15th symposium, Calculemus 2008, 7th international conference, MKM 2008, Birmingham, UK, July 28--August 1, 2008. Proceedings
- The practice of logical frameworks
- scientific article; zbMATH DE number 5883529 (Why is no real title available?)
- Secure the clones
- Expressive modular fine-grained concurrency specification
- Reasoning in Abella about structural operational semantics specifications
- scientific article; zbMATH DE number 1670739 (Why is no real title available?)
- The seventeen provers of the world. Foreword by Dana S. Scott..
- iRho: an imperative rewriting calculus
- Construction de schémas de flux s'appuyant sur une formulation cinétique champ par champ
- A certified lightweight non-interference Java bytecode verifier
- Formal Modelling of Emotions in BDI Agents
- Proof search with set variable instantiation in the calculus of constructions
- Integrating simplex with tableaux
- An assertional proof of the stability and correctness of Natural Mergesort
- A Coq formalization of the relational data model
- Proof-producing synthesis of CakeML from monadic HOL functions
- Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
- A library for formalization of linear error-correcting codes
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- Graph theory in Coq: minors, treewidth, and isomorphisms
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- On the bright side of type classes: instance arguments in Agda
- An assertional proof of red-black trees using Dafny
- scientific article; zbMATH DE number 1927420 (Why is no real title available?)
- Computer Aided Systems Theory – EUROCAST 2005
- scientific article; zbMATH DE number 1745043 (Why is no real title available?)
- A formal semantics of nested atomic sections with thread escape
- Call-by-value lambda calculus as a model of computation in Coq
- Categoricity results and large model constructions for second-order ZF in dependent type theory
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- Consistent subtyping for all
- Dualizing generalized algebraic data types by matrix transposition
- Failure is not an option. An exceptional type theory
- Let arguments go first
- Verified learning without regret. From algorithmic game theory to distributed systems with mechanized complexity guarantees
- The theory of contexts for first order and higher order abstract syntax
- Coq without type casts: a complete proof of Coq Modulo Theory
- An ordinal measure based procedure for termination of functions
- Mathematical knowledge representation: semantic models and formalisms
- Formal proof of a wave equation resolution scheme: the method error
- Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers
- Higman's lemma and its computational content
- Displayed Categories
- Flyspeck II: The basic linear programs
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- Network algebra for asynchronous dataflow∗
- Balancing Lists: A Proof Pearl
- Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
- On completeness of reducibility candidates as a semantics of strong normalization
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Type-theoretic approaches to ordinals
- Mechanically proving determinacy of hierarchical block diagram translations
- Barriers in concurrent separation logic: now with tool support!
- Extended initiality for typed abstract syntax
- Solving quantifier-free first-order constraints over finite sets and binary relations
- scientific article; zbMATH DE number 1424017 (Why is no real title available?)
- Tool-Based Verification of a Relational Vertex Coloring Program
- Self types for dependently typed lambda encodings
- Coinductive big-step operational semantics
- \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
- Para-disagreement logics and their implementation through embedding in Coq and SMT
- Eliminating dependent pattern matching without K
- A Linear Logical Framework in Hybrid (Invited Talk)
- Characteristics of de Bruijn’s early proof checker Automath
- A logical framework combining model and proof theory
- Libraries for generic programming in Haskell
- Herbrand constructivization for automated intuitionistic theorem proving
- Formal specification and proofs for the topology and classification of combinatorial surfaces
- A belief revision approach for argumentation-based negotiation agents
- Alcove
- A module calculus for Pure Type Systems
- Contractive signatures with recursive types, type parameters, and abstract types
- scientific article; zbMATH DE number 7649967 (Why is no real title available?)
- Formally verifying the solution to the Boolean Pythagorean triples problem
- RustHorn: CHC-based verification for Rust programs
- Some issues related to double rounding
- scientific article; zbMATH DE number 2085176 (Why is no real title available?)
- A formal verification technique for behavioural model-to-model transformations
- Cut branches before looking for bugs: certifiably sound verification on relaxed slices
- Verifying relative safety, accuracy, and termination for program approximations
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications
- Adjectival and adverbial modification: the view from modern type theories
- Typed lambda calculi and applications. International conference, TLCA '93, March 16--18, 1993, Utrecht, the Netherlands. Proceedings
- From types to sets by local type definition in higher-order logic
- Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms
This page was built for software: Coq
