Superposition with datatypes and codatatypes

DOI10.1007/978-3-319-94205-6_25MaRDI QIDQ1799098zbMATH OpenOpenAlexFDO

Authors Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard

Publication date 18 October 2018

Full work available at URL https://research.chalmers.se/en/publication/504169

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Supercompilation for datatypes
• Higher-order superposition for dependent types
• Superimpositions and Aspect-oriented Programming
• Advanced Functional Programming
• scientific article; zbMATH DE number 954811
• Intersection types and overloading
• scientific article; zbMATH DE number 897897
• Datatypes with shared selectors
• Type inference for record concatenation and multiple inheritance
• scientific article; zbMATH DE number 4180773

Cited in

(7)

• Superposition with first-class booleans and inprocessing clausification
• A decision procedure for (co)datatypes in SMT solvers
• A decision procedure for (co)datatypes in SMT solvers
• Coming to terms with quantified reasoning
• A comprehensive framework for saturation theorem proving
• A comprehensive framework for saturation theorem proving
• Some techniques for reasoning automatically on co-inductive data structures

Describes a project that uses

Uses Software

• Isabelle/HOL
• SMT-LIB
• RADA
• VAMPIRE
• z3
• Sledgehammer
• CVC4

This page was built for publication: Superposition with datatypes and codatatypes

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