Observatorio de I+D+i UPM

Descripción
Substitution is fundamental to the theory of logic and computation. Is substitution something that we define on syntax on a case-by-case basis, or can we turn the idea of substitution into a mathematical object? We give axioms for substitution and prove them sound and complete with respect to a canonical model. As corollaries we obtain a useful conservativity result, and prove that equality-up-to-substitution is a decidable relation on terms. These results involve subtle use of techniques both from rewriting and algebra. A special feature of our method is the use of nominal techniques. These give us access to a stronger assertion language, which includes so-called ‘freshness’ or ‘capture-avoidance’ conditions. This means that the sense in which we axiomatise substitution (and prove soundness and completeness) is particularly strong, while remaining quite general.
Internacional	Si
JCR del ISI	Si
Título de la revista	FORMAL ASPECTS OF COMPUTING
ISSN	0934-5043
Factor de impacto JCR	0,698
Información de impacto
Volumen	20
DOI
Número de revista	4
Desde la página	451
Hasta la página	479
Mes	ENERO
Ranking

Esta actividad pertenece a memorias de investigación

• Autor: Aad Mathijssen (Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands)
• Autor: Murdoch Gabbay (UPM)

• Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
• Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software