Higher-order superposition for dependent types

DOI10.1007/3-540-61464-8_47zbMath1504.68093OpenAlexW1565847800MaRDI QIDQ5055856

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

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

Related Items (2)

Explicit Contexts in LF (Extended Abstract) ⋮ Unnamed Item

Uses Software

• Elf

Cites Work

• Unnamed Item
• Unnamed Item
• Higher-order rewrite systems and their confluence
• Proving and applying program transformations expressed with second-order patterns
• The foundation of a generic theorem prover
• On theories with a combinatorial definition of 'equivalence'
• A framework for defining logics
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Towards a domain theory for termination proofs

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