scientific article; zbMATH DE number 6296049
From MaRDI portal
Publication:5417200
zbMath1288.68001MaRDI QIDQ5417200
Publication date: 16 May 2014
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Automatically proving equivalence by type-safe reflection ⋮ A Formalization of Properties of Continuous Functions on Closed Intervals ⋮ A certified program for the Karatsuba method to multiply polynomials ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ ANF preserves dependent types up to extensional equality ⋮ Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant ⋮ Hammer for Coq: automation for dependent type theory ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ Foundations of dependent interoperability ⋮ Auto in Agda ⋮ Verifying Selective CPS Transformation for Shift and Reset ⋮ System-level non-interference of constant-time cryptography. I: Model ⋮ Consistency-preserving refactoring of refinement structures in Event-B models ⋮ Extracting functional programs from Coq, in Coq ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ Naïve Type Theory ⋮ An automatically verified prototype of the Android permissions system ⋮ Mechanizing type environments in weak HOAS ⋮ Unnamed Item ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ The essence of ornaments ⋮ Unnamed Item ⋮ On a machine-checked proof for fraction arithmetic over a GCD domain ⋮ Friends with Benefits ⋮ Unnamed Item ⋮ Applicable Mathematics in a Minimal Computational Theory of Sets ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Bestow and atomic: concurrent programming using isolation, delegation and grouping ⋮ Fifty years of Hoare's logic ⋮ Unnamed Item ⋮ Implementing geometric algebra products with binary trees ⋮ Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics ⋮ Coq ⋮ Verified Operational Transformation for Trees ⋮ Mechanized metatheory revisited ⋮ Formalizing Scientifically Applicable Mathematics in a Definitional Framework ⋮ Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
Uses Software
