Proof-term synthesis on dependent-type systems via explicit substitutions

DOI10.1016/S0304-3975(00)00196-1zbMath0989.68019OpenAlexW2038670513MaRDI QIDQ5958764

No author found.

Publication date: 3 March 2002

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00196-1

zbMATH Keywords

lambda calculusexplicit substitutionshigher-order unificationproof synthesis

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Uses Software

• Coq
• Twelf
• ALF

Cites Work

• Mechanical procedure for proof construction via closed terms in typed \(\lambda\) calculus
• The calculus of constructions
• Unification under a mixed prefix
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Rewriting techniques and applications. 6th international conference, RTA-95, Kaiserslautern, Germany, April 5--7, 1995. Proceedings
• Higher order unification via explicit substitutions
• λ-calculi with explicit substitutions and composition which preserve β-strong normalization
• A simple proof of the undecidability of inhabitation in λP
• A framework for defining logics
• A Complete Proof Synthesis Method for the Cube of Type Systems
• Confluence properties of weak and strong calculi of explicit substitutions
• Explicit substitutions
• Higher-order unification with dependent function types
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof-term synthesis on dependent-type systems via explicit substitutions