scientific article; zbMATH DE number 2061716

MaRDI QIDQ4457464zbMATH OpenFDO

Authors Nicolas Oury

Publication date 22 March 2004

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2701/27010271.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 2003158
• Program extraction for mutable arrays
• Synthesis of ML programs in the system Coq
• Subset Coercions in Coq
• Extraction in Coq: An Overview

Cited in

(19)

• Mathematical knowledge representation: semantic models and formalisms
• Reasoning about iteration and recursion uniformly based on big-step semantics
• \textsc{Prawf}: an interactive proof system for program extraction
• Bidirectional grammars for machine-code decoding and encoding
• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• Extraction in Coq: An Overview
• A certified, corecursive implementation of exact real numbers
• Well-definedness and observational equivalence for inductive–coinductive programs
• Repairing time-determinism in the process algebra for hybrid systems
• The role of entropy in guiding a connection prover
• Deep Generation of Coq Lemma Names Using Elaborated Terms
• Implementing and reasoning about hash-consed data structures in Coq
• Implementing hash-consed structures in Coq
• scientific article; zbMATH DE number 2003158 (Why is no real title available?)
• Extracting functional programs from Coq, in Coq
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• Formally proving size optimality of sorting networks
• scientific article; zbMATH DE number 1070623 (Why is no real title available?)
• Equality checking for general type theories in Andromeda 2

Describes a project that uses

Uses Software

• Coq

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4457464)