Higher-order superposition for dependent types

DOI10.1007/3-540-61464-8_47MaRDI QIDQ5055856zbMATH OpenOpenAlexFDO

Authors Roberto Virga

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61464-8_47

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)

Recommendations

• Rewriting Techniques and Applications
• Higher-order unification with dependent function types
• Termination of rewriting in the Calculus of Constructions
• Superposition for full higher-order logic
• Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs

Cites work

• scientific article; zbMATH DE number 65531 (Why is no real title available?)
• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• A framework for defining logics
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Higher-order rewrite systems and their confluence
• On theories with a combinatorial definition of 'equivalence'
• Proving and applying program transformations expressed with second-order patterns
• The foundation of a generic theorem prover
• Towards a domain theory for termination proofs

Cited in

(4)

• scientific article; zbMATH DE number 7204440 (Why is no real title available?)
• Higher-order subtyping
• Superposition with datatypes and codatatypes
• Explicit contexts in LF (extended abstract)

Describes a project that uses

Uses Software

• Elf

This page was built for publication: Higher-order superposition for dependent types

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