scientific article; zbMATH DE number 2061716
From MaRDI portal
Publication:4457464
zbMATH Open1039.68543MaRDI QIDQ4457464FDOQ4457464
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
Title of this publication is not available (Why is that?)
Recommendations
Cited In (18)
- Mathematical knowledge representation: semantic models and formalisms
- Reasoning about iteration and recursion uniformly based on big-step semantics
- Bidirectional grammars for machine-code decoding and encoding
- \textsc{Prawf}: an interactive proof system for program extraction
- 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
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- The role of entropy in guiding a connection prover
- Implementing and reasoning about hash-consed data structures in Coq
- Implementing hash-consed structures in Coq
- Title not available (Why is that?)
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
- Formally proving size optimality of sorting networks
- Title not available (Why is that?)
- Equality checking for general type theories in Andromeda 2
Uses Software
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)
