The following pages link to Coq (Q12929):
Displaying 50 items.
- Innovations in computational type theory using Nuprl (Q865639) (← links)
- \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics (Q865658) (← links)
- Security types preserving compilation (Q865705) (← links)
- Mathematics of program construction. 8th international conference, MPC 2006, Kuressaare, Estonia, July 3--5, 2006. Proceedings. (Q873587) (← links)
- Resource operators for \(\lambda\)-calculus (Q876041) (← links)
- Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case (Q888469) (← links)
- A behavioural theory for a \(\pi\)-calculus with preorders (Q890617) (← links)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
- Mechanizing type environments in weak HOAS (Q897934) (← links)
- Type-based termination of generic programs (Q923883) (← links)
- Proofs of randomized algorithms in Coq (Q923886) (← links)
- A mechanized proof of the basic perturbation lemma (Q928666) (← links)
- Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves (Q928671) (← links)
- Logic and theory of algorithms. 4th conference on computability in Europe, CiE 2008, Athens, Greece, June 15--20, 2008. Proceedings (Q929188) (← links)
- Formalizing non-interference for a simple bytecode language in Coq (Q931434) (← links)
- Hybrid systems: computation and control. 11th international workshop, HSCC 2008, St. Louis, MO, USA, April 22--24, 2008. Proceedings (Q933702) (← links)
- Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof (Q944364) (← links)
- Formal verification of a C-like memory model and its uses for verifying program transformations (Q945054) (← links)
- Proof synthesis and reflection for linear arithmetic (Q945055) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- Abstraction-carrying code: a model for mobile code safety (Q949170) (← links)
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings (Q955386) (← links)
- 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 (Q958360) (← links)
- Optimization techniques for propositional intuitionistic logic and their implementation (Q959821) (← links)
- Modules over monads and initial semantics (Q964503) (← links)
- A verified framework for higher-order uncurrying optimizations (Q968367) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- The proof monad (Q974136) (← links)
- On Jensen's inequality and Hölder's inequality for \(g\)-expectation (Q974648) (← links)
- Intelligent computer mathematics. 10th international conference, AISC 2010, 17th symposium, Calculemus 2010, and 9th international conference, MKM 2010, Paris, France, July 5--10, 2010. Proceedings (Q983521) (← links)
- Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11--14, 2010. Proceedings (Q983522) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- HasCasl: integrated higher-order specification and program development (Q1006648) (← links)
- Programming languages and systems. 18th European symposium on programming, ESOP 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22--29, 2009. Proceedings (Q1008936) (← links)
- Coinductive big-step operational semantics (Q1012129) (← links)
- Certifying properties of an efficient functional program for computing Gröbner bases (Q1012152) (← links)
- The RISC ProofNavigator: a proving assistant for program verification in the classroom (Q1019024) (← links)
- Types for proofs and programs. International conference, TYPES 2008, Torino, Italy, March 26--29, 2008. Revised selected papers (Q1021638) (← links)
- Using computer algebra techniques for the specification, verification and synthesis of recursive programs (Q1025311) (← links)
- Intelligent computer mathematics. 16th symposium, Calculemus 2009, 8th international conference, MKM 2009, held as part of CICM 2009, Grand Bend, Canada, July 6--12, 2009. Proceedings (Q1028781) (← links)
- Adapting functional programs to higher order logic (Q1029815) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- A compact kernel for the calculus of inductive constructions (Q1040007) (← links)
- Formalizing Arrow's theorem (Q1040010) (← links)
- Data compression for proof replay (Q1040776) (← links)
