Ponencias en congresos:
Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables
Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables
Año:2009
Áreas de investigación
-
Lenguaje de programación
Datos
|
Descripción
|
|
|---|---|
| This paper develops the correspondence between equality reasoning with axioms using ¿-terms syntax, and reasoning using nominal terms syntax. Both syntaxes involve name-abstraction: ¿-terms represent functional abstraction; nominal terms represent atoms-abstraction in nominal sets. It is not evident how to relate the two syntaxes because their intended denotations are so different. We use universal algebra, the logic of equational reasoning, a logical foundation based on an equality judgement form which is spartan but which is suf¿ciently expressive to encode mathematics in theory and practice. We investigate how syntax, algebraic theories, and derivability relate across ¿-theories (algebra over ¿-terms) and nominal algebra theories. | |
|
Internacional
|
Si |
|
Nombre congreso
|
|
|
Tipo de participación
|
960 |
|
Lugar del congreso
|
|
|
Revisores
|
|
|
ISBN o ISSN
|
|
|
DOI
|
|
|
Fecha inicio congreso
|
|
|
Fecha fin congreso
|
|
|
Desde la página
|
|
|
Hasta la página
|
|
|
Título de las actas
|
|
Participantes
- Autor: Dominic P. Mulligan (Heriot-Watt University, Edinburgh, UK)
- Autor: Murdoch Gabbay (UPM)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
- 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
S2i 2023 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)