The following pages link to Coq (Q12929):
Displaying 50 items.
- The future of logic: foundation-independence (Q263104) (← links)
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (Q264193) (← links)
- Category theory, logic and formal linguistics: some connections, old and new (Q280832) (← links)
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- Four decades of {\textsc{Mizar}}. Foreword (Q286794) (← links)
- Reconsidering pairs and functions as sets (Q286796) (← links)
- Improving legibility of formal proofs based on the close reference principle is NP-hard (Q286805) (← links)
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems (Q287269) (← links)
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277) (← links)
- Interactive theorem proving. Preface of the special issue (Q287356) (← links)
- Verified abstract interpretation techniques for disassembling low-level self-modifying code (Q287369) (← links)
- Mechanizing a process algebra for network protocols (Q287372) (← links)
- Completeness and decidability results for CTL in constructive type theory (Q287375) (← links)
- Towards a certified version of the encyclopedia of triangle centers (Q294378) (← links)
- Challenging theorem provers with Mathematical Olympiad problems in solid geometry (Q294381) (← links)
- Algorithms for Kleene algebra with converse (Q299194) (← links)
- Supercompilation for Martin-Lof's type theory (Q300348) (← links)
- Theoretical aspects of computing -- ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24--31, 2016. Proceedings (Q327098) (← links)
- Proving tight bounds on univariate expressions with elementary functions in Coq (Q331615) (← links)
- Intuitionistic games: determinacy, completeness, and normalization (Q332080) (← links)
- Floating-point arithmetic on the test bench. How are verified numerical solutions calculated? (Q335016) (← links)
- Trustworthy variant derivation with translation validation for safety critical product lines (Q338617) (← links)
- Formal verification of concurrent programs with Read-write locks (Q351980) (← links)
- Certifying assembly programs with trails (Q352100) (← links)
- A two-valued logic for properties of strict functional programs allowing partial functions (Q352946) (← links)
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- Automated deduction in geometry. 9th international workshop, ADG 2012, Edinburgh, UK, September 17--19, 2012. Revised selected papers (Q365999) (← links)
- Automated reasoning with analytic tableaux and related methods. 22nd international conference, TABLEAUX 2013, Nancy, France, September 16--19, 2013. Proceedings (Q368052) (← links)
- On the role of formalization in computational mathematics (Q372699) (← links)
- Proceedings of the first international workshop on logical frameworks and meta-languages: theory and practice (LFMTP 2006), Seattle, WA, USA, August 16, 2006 (Q373630) (← links)
- On monads of exact reflective localizations of abelian categories (Q384299) (← links)
- Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11--13, 2013. Proceedings (Q385988) (← links)
- A mechanisation of some context-free language theory in HOL4 (Q386032) (← links)
- A scalable module system (Q391632) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Formal specification and proofs for the topology and classification of combinatorial surfaces (Q396466) (← links)
- Unifying sets and programs via dependent types (Q408534) (← links)
- On inter-deriving small-step and big-step semantics: a case study for storeless call-by-need evaluation (Q428886) (← links)
- A Church-style intermediate language for ML\(^{\text F}\) (Q428892) (← links)
- \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps (Q429596) (← links)
- Experiments in program verification using Event-B (Q432154) (← links)
- Mechanical reasoning about families of UTP theories (Q436368) (← links)
- Combining decision procedures by (model-)equality propagation (Q436376) (← links)
- JCML: A specification language for the runtime verification of Java card programs (Q436381) (← links)
- Certifying assembly with formal security proofs: the case of BBS (Q436406) (← links)
- The area method. A recapitulation (Q437042) (← links)
- A certified proof of the Cartan fixed point theorems (Q438546) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13--15, 2012. Proceedings (Q441467) (← links)
