The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors
Logic in Computer Science
2023-09-22 v1
Abstract
We prove the undecidability of the third order pattern matching problem in typed lambda-calculi with dependent types and in those with type constructors by reducing the second order unification problem to them.
Keywords
Cite
@article{arxiv.2309.11819,
title = {The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors},
author = {Gilles Dowek},
journal= {arXiv preprint arXiv:2309.11819},
year = {2023}
}
Comments
in French language