Higher-Order Pattern Anti-Unification in Linear Time

Home | About RECERCAT | Contact

Català | Castellano

All of RECERCAT

By Communities &
Collections By Defense Date By Authors By Titles By Subject

This Collection

By Defense Date By Authors By Titles By Subject

Statistics

View Statistics All RECERCAT

My RECERCAT

Other repositories directory

RECERCAT Home > Universitat de Girona > Documents de recerca > View document

To access the full text documents, please follow this link: http://hdl.handle.net/10256/14604

dc.contributor	Ministerio de Economía y Competitividad (Espanya)
dc.contributor.author	Baumgartner, Alexander
dc.contributor.author	Kutsia, Temur
dc.contributor.author	Levy, Jordi
dc.contributor.author	Villaret i Ausellé, Mateu
dc.date	2017-11-24T07:37:50Z
dc.date	2017-11-24T07:37:50Z
dc.date	2017-02-01
dc.identifier.citation	0168-7433 (versió paper)
dc.identifier.citation	1573-0670 (versió electrònica)
dc.identifier.citation	026315
dc.identifier.uri	http://hdl.handle.net/10256/14604
dc.format	application/pdf
dc.language.iso	eng
dc.publisher	Springer Verlag
dc.relation	https://doi.org/10.1007/s10817-016-9383-3
dc.relation	MINECO/PN 2013-2015/TIN2012-33042
dc.relation	MINECO/PE 2016-2018/TIN2015-66293-R
dc.relation	Reproducció digital del document publicat a: https://doi.org/10.1007/s10817-016-9383-3
dc.relation	Journal of Automated Reasoning, 2017, vol. 58, núm. 2, p. 293-310
dc.relation	Articles publicats (D-IMA)
dc.rights	Attribution 3.0 Spain
dc.rights	info:eu-repo/semantics/openAccess
dc.rights	http://creativecommons.org/licenses/by/3.0/es/
dc.subject	Algorismes computacionals
dc.subject	Computer algorithms
dc.subject	Lògica matemàtica
dc.subject	Logic, Symbolic and mathematical
dc.title	Higher-Order Pattern Anti-Unification in Linear Time
dc.type	info:eu-repo/semantics/article
dc.type	info:eu-repo/semantics/publishedVersion
dc.description.abstract	We present a rule-based Huet’s style anti-unification algorithm for simply typed lambda-terms, which computes a least general higher-order pattern generalization. For a pair of arbitrary terms of the same type, such a generalization always exists and is unique modulo α-equivalence and variable renaming. With a minor modification, the algorithm works for untyped lambda-terms as well. The time complexity of both algorithms is linear
dc.description.abstract	This research has been partially supported by the Austrian Science Fund (FWF) project SToUT (P 24087-N18), the Upper Austrian Government strategic program “Innovatives OÖ 2010plus”, the MINECO projects RASO (TIN2015-71799-C2-1-P) and HeLo (TIN2012-33042), the MINECO/FEDER UE project LoCoS (TIN2015-66293-R) and the UdG project MPCUdG2016/055

Show simple item record

All of RECERCAT

This Collection

Statistics

My RECERCAT

Related documents

Other documents of the same author