Pages that link to "Item:Q2881098"

The following pages link to A synthesis of the procedural and declarative styles of interactive theorem proving (Q2881098):

Displaying 26 items.

• miz3 (Q30463) (← links)
• Four decades of {\textsc{Mizar}}. Foreword (Q286794) (← links)
• Interactive theorem proving. Preface of the special issue (Q287356) (← links)
• Proceedings of the 7th workshop on user interfaces for theorem provers (UITP 2006), Seattle, WA, USA, August 21, 2006 (Q373628) (← links)
• Formal analysis of optical systems (Q475384) (← links)
• An introduction to mechanized reasoning (Q504394) (← links)
• A formal semantics of nested atomic sections with thread escape (Q1749114) (← links)
• CryptHOL: game-based proofs in higher-order logic (Q2175214) (← links)
• Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
• Proceedings of the 9th international workshop on user interfaces for theorem provers (UITP10), Edinburgh, UK, July 15, 2010 (Q2440903) (← links)
• From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
• (Q2729071) (← links)
• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0 (Q2819200) (← links)
• (Q3336730) (← links)
• Mizar: State-of-the-art and Beyond (Q3453119) (← links)
• The Abella Interactive Theorem Prover (System Description) (Q3541698) (← links)
• (Q4242056) (← links)
• (Q4539627) (← links)
• Formalizing Ordinal Partition Relations Using Isabelle/HOL (Q5094473) (← links)
• An Interactive Driver for Goal-directed Proof Strategies (Q5166499) (← links)
• Formal Proofs for Nonlinear Optimization (Q5195260) (← links)
• Integration of automated and interactive theorem proving in ILF (Q5234689) (← links)
• A Vernacular for Coherent Logic (Q5495937) (← links)
• Declarative Proof Translation (Short Paper) (Q5875449) (← links)
• Tools and Algorithms for the Construction and Analysis of Systems (Q5899057) (← links)