Normal higher-order termination
Visualitza/Obre
Cita com:
hdl:2117/79284
Tipus de documentArticle
Data publicació2015-03-01
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Abstract
We extend the termination proof methods based on reduction orderings to higher-order rewriting systems based on higher-order pattern matching. We accommodate, on the one hand, a weakly polymorphic, algebraic extension of Church's simply typed λ-calculus and, on the other hand, any use of eta, as a reduction, as an expansion, or as an equation. The user's rules may be of any type in this type system, either a base, functional, or weakly polymorphic type.
CitacióJouannaud, J., Rubio, A. Normal higher-order termination. "ACM transactions on computational logic", 01 Març 2015, vol. 16, núm. 2, p. 13:1-13:38.
ISSN1529-3785
Versió de l'editorhttp://dl.acm.org/citation.cfm?doid=2737801.2699913
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
jouannaud-rubio_normal.pdf | 588,9Kb | Visualitza/Obre |