Proof reuse with extended inductive types

DOI10.1007/978-3-540-30142-4_4MaRDI QIDQ5464662zbMATH OpenOpenAlexFDO

Authors Olivier Boite

Publication date 18 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b100400

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Generalization in type theory based proof assistants
• Constructor subtyping in the calculus of inductive constructions
• Meta-theory à la carte
• Structural recursive definitions in type theory
• scientific article; zbMATH DE number 2182487

Cited in

(10)

• Implementation techniques for inductive types in Plastic
• Information retrieval in a Coq proof library using type isomorphisms
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
• Tool support for proof engineering
• Proof principles for datatypes with iterated recursion
• Changing data structures in type theory: A study of natural numbers
• Generalization in type theory based proof assistants
• The -framework
• Theorem reuse by proof term transformation
• A type checker for a logical framework with union and intersection types (system description)

Describes a project that uses

Uses Software

• Coq
• Jakarta
• Nuprl

This page was built for publication: Proof reuse with extended inductive types

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