Pages that link to "Item:Q703860"
From MaRDI portal
The following pages link to Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (Q703860):
Displaying 50 items.
- Translation certification for smart contracts (Q2163161) (← links)
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (Q2198135) (← links)
- Relational characterisations of paths (Q2210868) (← links)
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support (Q2211865) (← links)
- A characterization of Moessner's sieve (Q2253190) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formally verifying the solution to the Boolean Pythagorean triples problem (Q2323449) (← links)
- Formalization of geometric algebra in HOL Light (Q2323452) (← links)
- Statistical properties of lambda terms (Q2327214) (← links)
- Mechanizing focused linear logic in Coq (Q2333326) (← links)
- Interactive verification of architectural design patterns in FACTum (Q2335950) (← links)
- Deciding Kleene algebra terms equivalence in Coq (Q2347910) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- Theorem of three circles in Coq (Q2351412) (← links)
- Premise selection for mathematics by corpus analysis and kernel methods (Q2352489) (← links)
- Formally verified certificate checkers for hardest-to-round computation (Q2352500) (← links)
- Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective (Q2354911) (← links)
- Theorem proving graph grammars with attributes and negative application conditions (Q2358623) (← links)
- Using relation-algebraic means and tool support for investigating and computing bipartitions (Q2360655) (← links)
- Analyzing program termination and complexity automatically with \textsf{AProVE} (Q2362493) (← links)
- Semantic representation of general topology in the Wolfram language (Q2364674) (← links)
- Automatically proving equivalence by type-safe reflection (Q2364699) (← links)
- Invariants for the FoCaL language (Q2379680) (← links)
- A brief account of runtime verification (Q2390027) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- Trusting computations: a mechanized proof from partial differential equations to actual program (Q2398899) (← links)
- Verifying a scheduling protocol of safety-critical systems (Q2424721) (← links)
- Some issues related to double rounding (Q2434938) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- Theorem-proving analysis of digital control logic interacting with continuous dynamics (Q2520681) (← links)
- Two cryptomorphic formalizations of projective incidence geometry (Q2631964) (← links)
- A decision procedure for linear ``big O'' equations (Q2642465) (← links)
- Code-carrying theories (Q2643124) (← links)
- Mechanizing common knowledge logic using COQ (Q2643149) (← links)
- Design and formal proof of a new optimal image segmentation program with hypermaps (Q2643883) (← links)
- Mechanized semantics for the clight subset of the C language (Q2655325) (← links)
- A formally verified compiler back-end (Q2655327) (← links)
- Crystal: Integrating structured queries into a tactic language (Q2655333) (← links)
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge (Q2663667) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- Certification of an exact worst-case self-stabilization time (Q2680867) (← links)
- Verification of the ROS NavFn planner using executable specification languages (Q2693303) (← links)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
- Reasoning in Abella about Structural Operational Semantics Specifications (Q2804943) (← links)
- Another Look at Function Domains (Q2805150) (← links)
- On the Formalization of Some Results of Context-Free Language Theory (Q2820703) (← links)
- Tests and Proofs for Enumerative Combinatorics (Q2827441) (← links)
- Mechanical Verification of a Constructive Proof for FLP (Q2829253) (← links)
- From Types to Sets by Local Type Definitions in Higher-Order Logic (Q2829259) (← links)
