The following pages link to Coq (Q12929):
Displaying 50 items.
- Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials (Q1733314) (← links)
- Refinement to certify abstract interpretations: illustrated on linearization for polyhedra (Q1739912) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- Programs as data structures in \(\lambda\)SF-calculus (Q1744389) (← links)
- Proving correctness of a compiler using step-indexed logical relations (Q1744423) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols (Q1744440) (← links)
- A formal semantics of nested atomic sections with thread escape (Q1749114) (← links)
- Flexary connectives in Mizar (Q1749141) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- Certified programs and proofs. Second international conference, CPP 2012, Kyoto, Japan, December 13--15, 2012. Proceedings (Q1758199) (← links)
- Certifying circuits in type theory (Q1764432) (← links)
- Theorem proving in higher order logics. 17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14--17, 2004. Proceedings. (Q1774486) (← links)
- Transitivity in coercive subtyping (Q1776403) (← links)
- Bestow and atomic: concurrent programming using isolation, delegation and grouping (Q1785860) (← links)
- Towards certified meta-programming with typed Template-Coq (Q1791140) (← links)
- Software tool support for modular reasoning in modal logics of actions (Q1791146) (← links)
- Backwards and forwards with separation logic (Q1791147) (← links)
- A Coq formalisation of SQL's execution engines (Q1791148) (← links)
- A Coq tactic for equality learning in linear arithmetic (Q1791149) (← links)
- The coinductive formulation of common knowledge (Q1791151) (← links)
- Tactics and certificates in Meta Dedukti (Q1791152) (← links)
- A formal proof of the minor-exclusion property for treewidth-two graphs (Q1791156) (← links)
- HOL Light QE (Q1791161) (← links)
- Efficient Mendler-style lambda-encodings in Cedille (Q1791163) (← links)
- Verification of PCP-related computational reductions in Coq (Q1791165) (← links)
- Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac} (Q1791170) (← links)
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) (Q1791178) (← links)
- Proof pearl: constructive extraction of cycle finding algorithms (Q1791179) (← links)
- Fast machine words in Isabelle/HOL (Q1791180) (← links)
- Relational parametricity and quotient preservation for modular (co)datatypes (Q1791181) (← links)
- Towards verified handwritten calculational proofs (short paper) (Q1791183) (← links)
- Formalizing implicative algebras in Coq (Q1791188) (← links)
- Towards formal foundations for game theory (Q1791194) (← links)
- A formal equational theory for call-by-push-value (Q1791198) (← links)
- Verified tail bounds for randomized programs (Q1791202) (← links)
- Verified memoization and dynamic programming (Q1791205) (← links)
- \(\mathrm{MDP + TA = PTA}\): probabilistic timed automata, formalized (short paper) (Q1791206) (← links)
- Formalization of a polymorphic subtyping algorithm (Q1791209) (← links)
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (Q1798665) (← links)
- Undecidability of equality for codata types (Q1798783) (← links)
- Concrete semantics with Coq and CoqHammer (Q1798946) (← links)
- A Coq formalization of digital filters (Q1798952) (← links)
- Exploring approximations for floating-point arithmetic using UppSAT (Q1799086) (← links)
- Verifying asymptotic time complexity of imperative programs in Isabelle (Q1799114) (← links)
- Theories as types (Q1799118) (← links)
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions (Q1799129) (← links)
- Typed lambda calculi and applications. 2nd international conference, TLCA '95, Edinburgh, GB, April 10--12, 1995. Proceedings (Q1805041) (← links)
- Mathematical knowledge management in HELM (Q1810904) (← links)
- A syntactic approach to foundational proof-carrying code (Q1826465) (← links)
- A trustworthy proof checker (Q1826468) (← links)
