Automating inversion of inductive predicates in Coq

DOI10.1007/3-540-61780-9_64MaRDI QIDQ4647573zbMATH OpenOpenAlexFDO

Authors Cristina Cornes, Delphine Terrasse

Publication date 15 January 2019

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

Full work available at URL https://doi.org/10.1007/3-540-61780-9_64

zbMATH Keywords

proof assistantlogic programminginductive definitionHorn clauseinductive type

Mathematics Subject Classification ID

Logic programming (68N17)

Recommendations

• Nominal Inversion Principles
• Handcrafted inversions made operational on operational semantics
• scientific article; zbMATH DE number 512790
• Automatic proofs by induction in theories without constructors
• Types for Proofs and Programs

Cites work

• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 591911 (Why is no real title available?)
• Automating inversion of inductive predicates in Coq
• Automatizing termination proofs of recursively defined functions
• The calculus of constructions

Cited in

(9)

• An application of co-inductive types in Coq: verification of the alternating bit protocol
• External and internal syntax of the \(\lambda \)-calculus
• Handcrafted inversions made operational on operational semantics
• Developing (meta)theory of \(\lambda\)-calculus in the theory of contexts
• Automating inversion of inductive predicates in Coq
• The theory of contexts for first order and higher order abstract syntax
• Nominal Inversion Principles
• \(\pi\)-calculus in (Co)inductive-type theory
• Builtin types viewed as inductive families

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Automating inversion of inductive predicates in Coq

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