scientific article; zbMATH DE number 2003158
From MaRDI portal
Publication:4435471
zbMath1023.68516MaRDI QIDQ4435471
Publication date: 12 November 2003
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2646/26460200.htm
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (18)
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ A formally verified compiler back-end ⋮ Mechanized Verification of CPS Transformations ⋮ Trace-based verification of imperative programs with I/O ⋮ Extracting functional programs from Coq, in Coq ⋮ A realizability interpretation of Church's simple theory of types ⋮ Map fusion for nested datatypes in intensional type theory ⋮ Unnamed Item ⋮ Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves ⋮ A Short Presentation of Coq ⋮ Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof ⋮ Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic ⋮ Realizability interpretation of proofs in constructive analysis ⋮ Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code ⋮ Tool Support for Proof Engineering ⋮ Theorem of three circles in Coq ⋮ Program extraction from normalization proofs
Uses Software
This page was built for publication:
