Observatorio de I+D+i UPM

Descripción
The Curry-Howard correspondence connects Natural Deduction derivation with the lambda-calculus. Predicates are types, derivations are terms. This supports reasoning from assumptions to conclusions, but we may want to reason `backwards' from the desired conclusion towards the assumptions. At intermediate stages we may have an `incomplete derivation', with `holes'. This is natural in informal practice; the challenge is to formalise it. To this end we use a one-and-a-halfth order technique based on nominal terms, with two levels of variable. Predicates are types, derivations are terms | and the two levels of variable are respectively the assumptions and the `holes' of an incomplete derivation.
Internacional	Si
Nombre congreso	Workshop on Logic, Language and Information in Computation (WoLLIC 2008)
Tipo de participación	960
Lugar del congreso	Edinburgh, Scotland
Revisores	No
ISBN o ISSN	978-3-540-69936-1
DOI	10.1007/978-3-540-69937-8
Fecha inicio congreso	01/07/2008
Fecha fin congreso	04/07/2008
Desde la página	179
Hasta la página	193
Título de las actas	Proceedings of Workshop on Logic, Language and Information in Computation (WoLLIC 2008)

Esta actividad pertenece a memorias de investigación

• Autor: Dominic P. Mulligan (Heriot-Watt University, Edinburgh)
• 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