|
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) |