The following pages link to Coq (Q12929):
Displaying 50 items.
- Dependent types for program termination verification (Q1850960) (← links)
- Structural cut elimination. I: Intuitionistic and classical logic (Q1854335) (← links)
- On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions (Q1854404) (← links)
- Planning proofs of equations in CCS (Q1857269) (← links)
- Automated verification of an audio-control protocol using UPPAAL (Q1858445) (← links)
- A proof of GMP square root (Q1868507) (← links)
- Automated proof construction in type theory using resolution (Q1868508) (← links)
- Proof reflection in Coq (Q1868509) (← links)
- External rewriting for skeptical proof assistants (Q1868511) (← links)
- Algorithms and proofs inheritance in the FOC language (Q1868513) (← links)
- A new implementation of Automath (Q1868514) (← links)
- A refinement of de Bruijn's formal language of mathematics (Q1876109) (← links)
- Theoretical aspects of computer software. 4th international symposium, TACS 2001, Sendai, Japan, October 29--31, 2001. Proceedings. (Q1880418) (← links)
- Operational semantics of the Java Card Virtual Machine (Q1881664) (← links)
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML (Q1881670) (← links)
- Formalizing the trading theorem in Coq (Q1882906) (← links)
- An experiment concerning mathematical proofs on computers with French undergraduate students (Q1884267) (← links)
- Nominal logic, a first order theory of names and binding (Q1887151) (← links)
- Implicit induction in conditional theories (Q1891255) (← links)
- A generic graphic framework for combining inference tools and editing proofs and formulae (Q1895412) (← links)
- Computation on abstract data types. The extensional approach, with an application to streams (Q1923575) (← links)
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- Trends in trends in functional programming 1999/2000 versus 2007/2008 (Q1929344) (← links)
- Type-specialized staged programming with process separation (Q1929349) (← links)
- Using two-point set statistics to estimate the diameter distribution in Boolean models with circular grains (Q1929971) (← links)
- Some general results about proof normalization (Q1931341) (← links)
- The first-order syntax of variadic functions (Q1934953) (← links)
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker (Q1935352) (← links)
- Foundational aspects of multiscale digitization (Q1935768) (← links)
- The HOL Light theory of Euclidean space (Q1945903) (← links)
- The locally nameless representation (Q1945914) (← links)
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (Q1945915) (← links)
- A solution to the PoplMark challenge based on de Bruijn indices (Q1945917) (← links)
- Nested abstract syntax in Coq (Q1945918) (← links)
- Formal metatheory of programming languages in the Matita interactive theorem prover (Q1945919) (← links)
- A list-machine benchmark for mechanized metatheory (Q1945921) (← links)
- From Kepler to Hales, and back to Hilbert (Q1946041) (← links)
- Formal verification of numerical programs: from C annotated programs to mechanical proofs (Q1949765) (← links)
- A validated real function calculus (Q1949769) (← links)
- Special issue: Formal proof (Q1961912) (← links)
- Certification of a type inference tool for ML: Damas-Milner within Coq (Q1961918) (← links)
- A full formalization of SLD-resolution in the calculus of inductive constructions (Q1961920) (← links)
- Some lambda calculus and type theory formalized (Q1961921) (← links)
- An assertional proof of red-black trees using Dafny (Q1984797) (← links)
- Univalent polymorphism (Q1987219) (← links)
- Automated deduction and knowledge management in geometry (Q1995808) (← links)
- Modular verification of programs with effects and effects handlers (Q1996433) (← links)
- (Co)inductive proof systems for compositional proofs in reachability logic (Q1996855) (← links)
- A linear algorithm for brick Wang tiling (Q2009470) (← links)
- A denotational semantics of textually aligned SPMD programs (Q2011201) (← links)
