scientific article; zbMATH DE number 2085174

MaRDI QIDQ4736398zbMATH OpenFDO

Authors Nicolas Magaud, Yves Bertot

Publication date 9 August 2004

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

zbMATH Keywords

automatic translation toolCoq proof assistantinductive definitionsnatural numbersproof structure

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Changing data representation within the \textsf{Coq} system
• Theorem Proving in Higher Order Logics
• Automating change of representation for proofs in discrete mathematics (extended version)
• Working with Mathematical Structures in Type Theory
• Automating Change of Representation for Proofs in Discrete Mathematics

Cited in

(6)

• Changing types: information dynamics for qualitative type spaces
• Automating change of representation for proofs in discrete mathematics (extended version)
• Constructive membership predicates as index types
• Changing data representation within the \textsf{Coq} system
• Ornaments for Proof Reuse in Coq
• Automatically generalizing proofs and statements

Describes a project that uses

Uses Software

• ALF
• 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 Q4736398)