Memorias de investigación
Communications at congresses:
One-and-a-halfth order terms: Curry-Howard and incomplete derivations.
Year:2008

Research Areas
  • Programming language

Information
Abstract
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.
International
Si
Congress
Workshop on Logic, Language and Information in Computation (WoLLIC 2008)
960
Place
Edinburgh, Scotland
Reviewers
No
ISBN/ISSN
978-3-540-69936-1
10.1007/978-3-540-69937-8
Start Date
01/07/2008
End Date
04/07/2008
From page
179
To page
193
Proceedings of Workshop on Logic, Language and Information in Computation (WoLLIC 2008)
Participants
  • Autor: Dominic P. Mulligan Heriot-Watt University, Edinburgh
  • Autor: Murdoch Gabbay . UPM

Research Group, Departaments and Institutes related
  • 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