The following pages link to Coq (Q12929):
Displaying 50 items.
- Event algebra for transition systems composition application to timed automata (Q1656550) (← links)
- Certified universal gathering in \(\mathbb {R}^2\) for oblivious mobile robots (Q1660934) (← links)
- Towards a unified ordering for superposition-based automated reasoning (Q1662244) (← links)
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
- Toward compositional verification of interruptible OS kernels and device drivers (Q1663225) (← links)
- VST-Floyd: a separation logic tool to verify correctness of C programs (Q1663238) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Formally verified algorithms for upper-bounding state space diameters (Q1663245) (← links)
- Regular language representations in the constructive type theory of Coq (Q1663246) (← links)
- The formalization of discrete Fourier transform in HOL (Q1666338) (← links)
- Nominal C-unification (Q1671156) (← links)
- A certified reference validation mechanism for the permission model of Android (Q1671162) (← links)
- Formally verifying exceptions for low-level code with separation logic (Q1683698) (← links)
- Foundational (co)datatypes and (co)recursion for higher-order logic (Q1687535) (← links)
- Formalization of the Lindemann-Weierstrass theorem (Q1687717) (← links)
- CompCertS: a memory-aware verified C compiler using pointer as integer semantics (Q1687720) (← links)
- Formal verification of a floating-point expansion renormalization algorithm (Q1687723) (← links)
- FoCaLiZe and Dedukti to the rescue for proof interoperability (Q1687726) (← links)
- A formal proof in Coq of Lasalle's invariance principle (Q1687728) (← links)
- Certifying standard and stratified Datalog inference engines in SSReflect (Q1687733) (← links)
- Weak call-by-value lambda calculus as a model of computation in Coq (Q1687735) (← links)
- Bellerophon: tactical theorem proving for hybrid systems (Q1687737) (← links)
- Categoricity results for second-order ZF in dependent type theory (Q1687749) (← links)
- Making PVS accessible to generic services by interpretation in a universal format (Q1687752) (← links)
- Typing total recursive functions in Coq (Q1687755) (← links)
- Schulze voting as evidence carrying computation (Q1687758) (← links)
- Verified spilling and translation validation with repair (Q1687761) (← links)
- A formalisation of consistent consequence for Boolean equation systems (Q1687766) (← links)
- Verifying a concurrent garbage collector using a rely-guarantee methodology (Q1687774) (← links)
- Gauge integral (Q1688749) (← links)
- Meaning explanations at higher dimension (Q1688954) (← links)
- A formal C memory model for separation logic (Q1694027) (← links)
- Formally proving size optimality of sorting networks (Q1694569) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- Modular deductive verification of multiprocessor hardware designs (Q1702892) (← links)
- Selected extended papers of VSTTE 2016 (Q1703005) (← links)
- The matrix reproved (verification pearl) (Q1703015) (← links)
- Adding logic to the toolbox of molecular biology (Q1705298) (← links)
- (Mathematical) logic for systems biology (invited paper) (Q1706576) (← links)
- Formal proof of a machine closed theorem in Coq (Q1714805) (← links)
- Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms (Q1722642) (← links)
- The flow of ODEs: formalization of variational equation and Poincaré map (Q1722644) (← links)
- From types to sets by local type definition in higher-order logic (Q1722645) (← links)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647) (← links)
- Formally verified approximations of definite integrals (Q1722649) (← links)
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq (Q1725841) (← links)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
- Verifying OpenJDK's sort method for generic collections (Q1725846) (← links)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 (Q1731963) (← links)
- Intensional computation with higher-order functions (Q1733061) (← links)
