The following pages link to Coq (Q12929):
Displaying 50 items.
- Cut branches before looking for bugs: certifiably sound verification on relaxed slices (Q682366) (← links)
- Adjectival and adverbial modification: the view from modern type theories (Q683682) (← links)
- Typed lambda calculi and applications. International conference, TLCA '93, March 16--18, 1993, Utrecht, the Netherlands. Proceedings (Q684571) (← links)
- Proofs, programs, processes (Q693063) (← links)
- Theorem proving in higher order logics. 15th international conference, TPHOLs 2002, Hampton, VA, USA, August 20--23, 2002. Proceedings (Q701699) (← links)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (Q703860) (← links)
- Computer theorem proving in mathematics (Q704001) (← links)
- Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 -- May 4, 2003. Revised selected papers. (Q704168) (← links)
- Mathematical knowledge management. Third international conference, MKM 2004, Białowieża, Poland, September 19--21, 2004. Proceedings. (Q704809) (← links)
- Floating-point arithmetic in the Coq system (Q714617) (← links)
- The world's shortest correct exact real arithmetic program? (Q714620) (← links)
- ``Backward'' coinduction, Nash equilibrium and the rationality of escalation (Q715039) (← links)
- Frontiers of combining systems. 7th international symposium, FroCoS 2009, Trento, Italy, September 16--18, 2009. Proceedings (Q731475) (← links)
- Building program construction and verification tools from algebraic principles (Q736461) (← links)
- Cardinality of relations with applications (Q738869) (← links)
- Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22--25, 2016. Proceedings (Q739160) (← links)
- Implementing type systems for the IDE with Xsemantics (Q739624) (← links)
- Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician (Q740456) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- Isomorphism is equality (Q740487) (← links)
- Implementing geometric algebra products with binary trees (Q742367) (← links)
- A belief revision approach for argumentation-based negotiation agents (Q747516) (← links)
- Mechanizing bisimulation theorems for relation-changing logics in Coq (Q777873) (← links)
- Two case studies of semantics execution in Maude: CCS and LOTOS (Q816216) (← links)
- Program extraction from normalization proofs (Q817701) (← links)
- A certified, corecursive implementation of exact real numbers (Q817858) (← links)
- Admissible digit sets (Q817861) (← links)
- The seventeen provers of the world. Foreword by Dana S. Scott.. (Q819987) (← links)
- Vampire with a brain is a good ITP hammer (Q831938) (← links)
- High-level modelling for typed functional programming (Q832100) (← links)
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) (Q832157) (← links)
- Theory exploration powered by deductive synthesis (Q832255) (← links)
- Sound verification procedures for temporal properties of infinite-state systems (Q832273) (← links)
- Towards a trustworthy semantics-based language framework via proof generation (Q832282) (← links)
- Automatic generation and validation of instruction encoders and decoders (Q832306) (← links)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms (Q832310) (← links)
- Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings (Q834373) (← links)
- Certifying low-level programs with hardware interrupts and preemptive threads (Q835764) (← links)
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps (Q839032) (← links)
- Coq formalization of the higher-order recursive path ordering (Q843949) (← links)
- Directly reflective meta-programming (Q848742) (← links)
- A minimalistic look at widening operators (Q848744) (← links)
- Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
- Functional and logic programming. 8th international symposium, FLOPS 2006, Fuji-Susono, Japan, April 24--26, 2006. Proceedings. (Q855052) (← links)
- An effective proof of the well-foundedness of the multiset path ordering (Q857884) (← links)
- Formal proof of a program: find (Q858911) (← links)
- Proof-carrying code from certified abstract interpretation and fixpoint compression (Q860842) (← links)
- Choices in representation and reduction strategies for lambda terms in intensional contexts (Q861365) (← links)
- Tool-assisted specification and verification of typed low-level languages (Q861687) (← links)
- Explaining Gabriel-Zisman localization to the computer (Q861700) (← links)
