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.
- Formal verification of a C-like memory model and its uses for verifying program transformations (Q945054) (← links)
- Proof synthesis and reflection for linear arithmetic (Q945055) (← links)
- Optimization techniques for propositional intuitionistic logic and their implementation (Q959821) (← links)
- A verified framework for higher-order uncurrying optimizations (Q968367) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- Coinductive big-step operational semantics (Q1012129) (← links)
- Certifying properties of an efficient functional program for computing Gröbner bases (Q1012152) (← links)
- Using computer algebra techniques for the specification, verification and synthesis of recursive programs (Q1025311) (← links)
- Adapting functional programs to higher order logic (Q1029815) (← links)
- A compact kernel for the calculus of inductive constructions (Q1040007) (← links)
- How testing helps to diagnose proof failures (Q1624590) (← links)
- Tests and proofs for custom data generators (Q1624592) (← links)
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (Q1640636) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- How to get more out of your oracles (Q1687729) (← links)
- Typing total recursive functions in Coq (Q1687755) (← links)
- Schulze voting as evidence carrying computation (Q1687758) (← links)
- Formally proving size optimality of sorting networks (Q1694569) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- The matrix reproved (verification pearl) (Q1703015) (← links)
- Adding logic to the toolbox of molecular biology (Q1705298) (← links)
- From types to sets by local type definition in higher-order logic (Q1722645) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- A formal semantics of nested atomic sections with thread escape (Q1749114) (← links)
- Undecidability of equality for codata types (Q1798783) (← links)
- Foundational aspects of multiscale digitization (Q1935768) (← links)
- A list-machine benchmark for mechanized metatheory (Q1945921) (← links)
- Formal verification of numerical programs: from C annotated programs to mechanical proofs (Q1949765) (← links)
- An assertional proof of red-black trees using Dafny (Q1984797) (← links)
- Automated deduction and knowledge management in geometry (Q1995808) (← links)
- (Co)inductive proof systems for compositional proofs in reachability logic (Q1996855) (← links)
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check (Q2013318) (← links)
- Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
- A formally verified floating-point implementation of the compact position reporting algorithm (Q2024357) (← links)
- A generic and executable formalization of signature-based Gröbner basis algorithms (Q2028994) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Certified abstract cost analysis (Q2044174) (← links)
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- A symbolic-numeric validation algorithm for linear ODEs with Newton-Picard method (Q2051589) (← links)
- Integrating induction and coinduction via closure operators and proof cycles (Q2096458) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- \textsc{Prawf}: an interactive proof system for program extraction (Q2106598) (← links)
- \texttt{slepice}: towards a verified implementation of type theory in type theory (Q2119108) (← links)
- Certifying choreography compilation (Q2119966) (← links)
- The effects of effects on constructivism (Q2133168) (← links)
- Generalized arrays for Stainless frames (Q2152661) (← links)
- Trace semantics and algebraic laws for MCA ARMv8 architecture based on UTP (Q2154026) (← links)
- Program logic for higher-order probabilistic programs in Isabelle/HOL (Q2163157) (← links)
