Automating inversion of inductive predicates in Coq
From MaRDI portal
Publication:4647573
DOI10.1007/3-540-61780-9_64zbMath1407.68433OpenAlexW1849370879MaRDI QIDQ4647573
Delphine Terrasse, Cristina Cornes
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
Related Items
Automating inversion of inductive predicates in Coq ⋮ An application of co-inductive types in Coq: Verification of the alternating bit protocol ⋮ External and internal syntax of the \(\lambda \)-calculus ⋮ Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types. ⋮ The Theory of Contexts for First Order and Higher Order Abstract Syntax ⋮ \(\pi\)-calculus in (Co)inductive-type theory
Uses Software
Cites Work
