The following pages link to Coq (Q12929):
Displaying 50 items.
- Repairing time-determinism in the process algebra for hybrid systems (Q442292) (← links)
- A case study in formalizing projective geometry in Coq: Desargues theorem (Q448975) (← links)
- Designing and proving correct a convex hull algorithm with hypermaps in Coq (Q448980) (← links)
- Relational and algebraic methods in computer science. 13th international conference, RAMiCS 2012, Cambridge, UK, September 17--20, 2012. Proceedings (Q450615) (← links)
- Fences in weak memory models (Q453523) (← links)
- Polynomial function intervals for floating-point software verification (Q457251) (← links)
- Binary trees as a computational framework (Q461478) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- The termination of the higher-dimensional tarai functions (Q477602) (← links)
- Impossibility of gathering, a certification (Q483063) (← links)
- Formal study of functional orbits in finite domains (Q483296) (← links)
- Interactive theorem proving. 6th international conference, ITP 2015, Nanjing, China, August 24--27, 2015. Proceedings (Q492141) (← links)
- Tarski geometry axioms. II (Q502683) (← links)
- Tarski geometry axioms (Q502700) (← links)
- A generic framework for symbolic execution: a coinductive approach (Q507361) (← links)
- Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
- A language-independent proof system for full program equivalence (Q510898) (← links)
- Constructions of categories of setoids from proof-irrelevant families (Q512135) (← links)
- A robust high-order Lagrange-projection like scheme with large time steps for the isentropic Euler equations (Q512161) (← links)
- Maximally permissive controlled system synthesis for non-determinism and modal logic (Q513185) (← links)
- Homography in \(\mathbb{R}\mathbb{P}^2\) (Q520382) (← links)
- Verification of population protocols (Q523133) (← links)
- On graph rewriting, reduction, and evaluation in the presence of cycles (Q526460) (← links)
- Elementary recursive quantifier elimination based on Thom encoding and sign determination (Q529166) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- Automated deduction in geometry. 7th international workshop, ADG 2008, Shanghai, China, September 22--24, 2008. Revised papers (Q532630) (← links)
- Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings (Q555659) (← links)
- Intelligent computer mathematics. 11th international conference, AISC 2012, 19th symposium, Calculemus 2012, 5th international workshop, DML 2012, 11th international conference, MKM 2012, systems and projects, held as part of CICM 2012, Bremen, Germany, J (Q592091) (← links)
- Formal and efficient primality proofs by use of computer algebra oracles (Q597112) (← links)
- An algebraic approach to the design of compilers for object-oriented languages (Q607399) (← links)
- Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving (Q617922) (← links)
- Trace-based verification of imperative programs with I/O (Q617977) (← links)
- Algebraic methodology and software technology. 13th international conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23--25, 2010. Revised selected papers (Q619012) (← links)
- Implementation and application of automata. 15th international conference, CIAA 2010, Winnipeg, MB, Canada, August 12--15, 2010. Revised selected papers (Q624908) (← links)
- Map fusion for nested datatypes in intensional type theory (Q627204) (← links)
- Effective homology of bicomplexes, formalized in Coq (Q631755) (← links)
- Certifying compilers using higher-order theorem provers as certificate checkers (Q633302) (← links)
- Extracting the resolution algorithm from a completeness proof for the propositional calculus (Q636273) (← links)
- Mathematical analysis of stage-based programmable logic controller (Q636562) (← links)
- Coalgebras in functional programming and type theory (Q639643) (← links)
- Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14--18, 2011. Proceedings (Q643151) (← links)
- Automated deduction in geometry. 8th international workshop, ADG 2010, Munich, Germany, July 22--24, 2010. Revised selected papers (Q645925) (← links)
- Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7--9, 2011. Proceedings (Q646371) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (Q670696) (← links)
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (Q670699) (← links)
- Amortized complexity verified (Q670702) (← links)
- Verifying relative safety, accuracy, and termination for program approximations (Q682353) (← links)
- A formal verification technique for behavioural model-to-model transformations (Q682361) (← links)
