Coq

swMATH161WikidataQ1131652MaRDI QIDQ12929

No author found.

Described by source

No records found.

Related Items (only showing first 100 items - show all)

Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system ⋮ Category theory, logic and formal linguistics: some connections, old and new ⋮ A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Four decades of {\textsc{Mizar}}. Foreword ⋮ Reconsidering pairs and functions as sets ⋮ Improving legibility of formal proofs based on the close reference principle is NP-hard ⋮ Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Interactive theorem proving. Preface of the special issue ⋮ Verified abstract interpretation techniques for disassembling low-level self-modifying code ⋮ Mechanizing a process algebra for network protocols ⋮ Completeness and decidability results for CTL in constructive type theory ⋮ Towards a certified version of the encyclopedia of triangle centers ⋮ Challenging theorem provers with Mathematical Olympiad problems in solid geometry ⋮ Algorithms for Kleene algebra with converse ⋮ Supercompilation for Martin-Lof's type theory ⋮ Theoretical aspects of computing -- ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24--31, 2016. Proceedings ⋮ Proving tight bounds on univariate expressions with elementary functions in Coq ⋮ Intuitionistic games: determinacy, completeness, and normalization ⋮ Floating-point arithmetic on the test bench. How are verified numerical solutions calculated? ⋮ Trustworthy variant derivation with translation validation for safety critical product lines ⋮ Formal verification of concurrent programs with Read-write locks ⋮ Certifying assembly programs with trails ⋮ A two-valued logic for properties of strict functional programs allowing partial functions ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Formal and efficient primality proofs by use of computer algebra oracles ⋮ Automated deduction in geometry. 9th international workshop, ADG 2012, Edinburgh, UK, September 17--19, 2012. Revised selected papers ⋮ Automated reasoning with analytic tableaux and related methods. 22nd international conference, TABLEAUX 2013, Nancy, France, September 16--19, 2013. Proceedings ⋮ On the role of formalization in computational mathematics ⋮ Proceedings of the first international workshop on logical frameworks and meta-languages: theory and practice (LFMTP 2006), Seattle, WA, USA, August 16, 2006 ⋮ An algebraic approach to the design of compilers for object-oriented languages ⋮ On monads of exact reflective localizations of abelian categories ⋮ Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11--13, 2013. Proceedings ⋮ A mechanisation of some context-free language theory in HOL4 ⋮ A scalable module system ⋮ Intuitionistic completeness of first-order logic ⋮ Formal specification and proofs for the topology and classification of combinatorial surfaces ⋮ Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving ⋮ Trace-based verification of imperative programs with I/O ⋮ Algebraic methodology and software technology. 13th international conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23--25, 2010. Revised selected papers ⋮ Unifying sets and programs via dependent types ⋮ Implementation and application of automata. 15th international conference, CIAA 2010, Winnipeg, MB, Canada, August 12--15, 2010. Revised selected papers ⋮ Map fusion for nested datatypes in intensional type theory ⋮ Effective homology of bicomplexes, formalized in Coq ⋮ Certifying compilers using higher-order theorem provers as certificate checkers ⋮ On inter-deriving small-step and big-step semantics: a case study for storeless call-by-need evaluation ⋮ A Church-style intermediate language for ML\(^{\text F}\) ⋮ \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps ⋮ Experiments in program verification using Event-B ⋮ Extracting the resolution algorithm from a completeness proof for the propositional calculus ⋮ Mathematical analysis of stage-based programmable logic controller ⋮ Mechanical reasoning about families of UTP theories ⋮ Combining decision procedures by (model-)equality propagation ⋮ JCML: A specification language for the runtime verification of Java card programs ⋮ Certifying assembly with formal security proofs: the case of BBS ⋮ The area method. A recapitulation ⋮ A certified proof of the Cartan fixed point theorems ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Coalgebras in functional programming and type theory ⋮ Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13--15, 2012. Proceedings ⋮ Repairing time-determinism in the process algebra for hybrid systems ⋮ Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14--18, 2011. Proceedings ⋮ A case study in formalizing projective geometry in Coq: Desargues theorem ⋮ Designing and proving correct a convex hull algorithm with hypermaps in Coq ⋮ Relational and algebraic methods in computer science. 13th international conference, RAMiCS 2012, Cambridge, UK, September 17--20, 2012. Proceedings ⋮ Automated deduction in geometry. 8th international workshop, ADG 2010, Munich, Germany, July 22--24, 2010. Revised selected papers ⋮ Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7--9, 2011. Proceedings ⋮ Fences in weak memory models ⋮ Polynomial function intervals for floating-point software verification ⋮ Binary trees as a computational framework ⋮ Verification conditions for source-level imperative programs ⋮ Representing model theory in a type-theoretical logical framework ⋮ Recycling proof patterns in Coq: case studies ⋮ The termination of the higher-dimensional tarai functions ⋮ Impossibility of gathering, a certification ⋮ Formal study of functional orbits in finite domains ⋮ Interactive theorem proving. 6th international conference, ITP 2015, Nanjing, China, August 24--27, 2015. Proceedings ⋮ Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ Amortized complexity verified ⋮ Tarski geometry axioms. II ⋮ Tarski geometry axioms ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ A language-independent proof system for full program equivalence ⋮ Constructions of categories of setoids from proof-irrelevant families ⋮ A robust high-order Lagrange-projection like scheme with large time steps for the isentropic Euler equations ⋮ Maximally permissive controlled system synthesis for non-determinism and modal logic ⋮ Verifying relative safety, accuracy, and termination for program approximations ⋮ A formal verification technique for behavioural model-to-model transformations ⋮ Homography in \(\mathbb{R}\mathbb{P}^2\) ⋮ Verification of population protocols ⋮ On graph rewriting, reduction, and evaluation in the presence of cycles ⋮ Elementary recursive quantifier elimination based on Thom encoding and sign determination ⋮ A framework for developing stand-alone certifiers ⋮ Automated deduction in geometry. 7th international workshop, ADG 2008, Shanghai, China, September 22--24, 2008. Revised papers ⋮ Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings ⋮ 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, July 8--13, 2012. Proceedings ⋮ The future of logic: foundation-independence

This page was built for software: Coq