The following pages link to Coq (Q12929):
Displaying 50 items.
- A constructive approach to sequential Nash equilibria (Q1045892) (← links)
- Verifying programs in the calculus of inductive constructions (Q1267035) (← links)
- Types for proofs and programs. International workshop TYPES '96, Aussois, France, December 15--19, 1996. Selected papers (Q1270497) (← links)
- A note on complexity measures for inductive classes in constructive type theory (Q1271558) (← links)
- Automated synthesis of recursive programs from a \(\forall\exists\) logical specification (Q1272617) (← links)
- A compositional \(\mu\)-calculus proof system for statecharts processes (Q1285661) (← links)
- On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations (Q1302298) (← links)
- Set theory for verification. I: From foundations to functions (Q1319386) (← links)
- Singleton, union, and intersection types for program extraction (Q1322477) (← links)
- Synthesis of ML programs in the system Coq (Q1322847) (← links)
- Inductive families (Q1336951) (← links)
- Focus points and convergent process operators: A proof strategy for protocol verification (Q1349249) (← links)
- Formalizing process algebraic verifications in the calculus of constructions (Q1355748) (← links)
- Automated theorem proving by test set induction (Q1355757) (← links)
- Indexed types (Q1389626) (← links)
- A compared study of two correctness proofs for the standardized algorithm of ABR conformance (Q1395676) (← links)
- Software security -- theories and systems. Mext-NSF-JSPS international symposium, ISSS 2002, Tokyo, Japan, November 8--10, 2002. Revised papers (Q1397223) (← links)
- A rewriting approach to satisfiability procedures. (Q1401930) (← links)
- A constructive algebraic hierarchy in Coq. (Q1404425) (← links)
- Types for proofs and programs. International workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24--28, 2002. Selected papers (Q1408067) (← links)
- Theorem proving in higher order logics. 16th international conference, TPHOLs 2003, Rome, Italy, September 8--12, 2003. Proceedings (Q1416071) (← links)
- Typed lambda calculi and applications. 6th international conference, TLCA 2003, Valencia, Spain, June 10--12, 2003. Proceedings (Q1418347) (← links)
- Formalizing mathematics in higher-order logic: A case study in geometric modelling (Q1575663) (← links)
- The calculus of constructions as a framework for proof search with set variable instantiation (Q1575927) (← links)
- Encoding modal logics in logical frameworks (Q1577344) (← links)
- Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings (Q1578436) (← links)
- \(\pi\)-calculus in (Co)inductive-type theory (Q1589654) (← links)
- Logic for programming and automated reasoning. 7th international conference, LPAR 2000, Reunion Island, France, November 6--10, 2000. Proceedings (Q1589868) (← links)
- Types for proofs and programs. 3rd international workshop, TYPES '99, Lökeberg, Sweden, June 12--16, 1999. Selected papers (Q1591869) (← links)
- Advances in computing science - ASIAN 2000. 6th Asian computing science conference, Penang, Malaysia, November 25--27, 2000. Proceedings (Q1591870) (← links)
- A machine-checked implementation of Buchberger's algorithm (Q1595926) (← links)
- Types for proofs and programs. International workshop, TYPES 2000, Durham, GB, December 8--12, 2000. Selected papers (Q1601174) (← links)
- Proof planning for strategy development (Q1601860) (← links)
- Correctness of Java card method lookup via logical relations (Q1603654) (← links)
- On the numerical solution to two-fluid models via a cell-centered finite volume method (Q1604109) (← links)
- Evaluating general purpose automated theorem proving systems (Q1606324) (← links)
- A modal and relevance logic for qualitative spatial reasoning (Q1617813) (← links)
- A set solver for finite set relation algebra (Q1617837) (← links)
- Formal verification of a geometry algorithm: A quest for abstract views and symmetry in coq proofs (Q1623113) (← links)
- How testing helps to diagnose proof failures (Q1624590) (← links)
- Tests and proofs for custom data generators (Q1624592) (← links)
- A semi-automatic proof of strong connectivity (Q1630027) (← links)
- A relational model for probabilistic connectors based on timed data distribution streams (Q1631223) (← links)
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (Q1640636) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Formalization of the arithmetization of Euclidean plane geometry and applications (Q1640646) (← links)
- Formal verification of the correspondence between call-by-need and call-by-name (Q1648863) (← links)
- Program extraction for mutable arrays (Q1648867) (← links)
- Verifying higher-order functions with tree automata (Q1653017) (← links)
- Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings (Q1653699) (← links)
