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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bloo, R., Kamareddine, F., Laan, T., Nederpelt, R.: Parameters in pure type systems. In: Rajsbaum, S. (ed.) LATIN 2002. LNCS, vol. 2286, pp. 371–385. Springer, Heidelberg (2002)
Bognar, M.: Contexts in Lambda Calculus. PhD thesis, Vrije Universiteit Amsterdam (2002)
Cheney, J.: Nominal logic and abstract syntax. SIGACT News (logic column 14) 36(4), 47–69 (2005)
de Bruijn, N.G.: A survey of the project AUTOMATH. In: Hindley, Seldin (eds.) To H.B.Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, London (1980)
Fernández, M., Gabbay, M.J.: Curry-style types for nominal rewriting. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502. Springer, Heidelberg (2007)
Fernández, M., Gabbay, M.J.: Nominal rewriting. Information and Computation 205, 917–965 (2007)
Gabbay, M.J., Lengrand, S.: The lambda-context calculus. ENTCS 196, 19–35 (2008)
Gabbay, M.J., Mathijssen, A.: One-and-a-halfth-order logic. Journal of Logic and Computation (November 2007)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13(3–5), 341–363 (2001)
Huet, G.: Higher order unification 30 years later. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 3–12. Springer, Heidelberg (2002)
Jojgov, G.I.: Holes with binding power. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 162–181. Springer, Heidelberg (2003)
Mathijssen, A.: Logical Calculi for Reasoning with Binding. PhD thesis, Technische Universiteit Eindhoven (2007)
McBride, C.: Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh (1999)
Miller, D.: Unification under a mixed prefix. Journal of Symbolic Computation 14(4), 321–358 (1992)
Miller, D., Saurin, A.: A game semantics for proof search: preliminary results. In: MFPS XXI. ENTCS, vol. 155, pp. 543–563 (2006)
Nordstrom, B., Petersson, K., Smith, J.M.: Programming in Martin-Lof’s Type Theory. Int’l Series of Monographs on Computer Science, vol. 7. Clarendon Press, Oxford (1990)
Poernomo, I.H., Crossley, J.N., Wirsing, M.: Adapting Proofs-as-Programs: The Curry–Howard Protocol. Monographs in Computer Science, vol. XII (2005)
Pitts, A.M.: Equivariant syntax and semantics. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 32–36. Springer, Heidelberg (2002)
Pym, D.J., Ritter, E.: A games semantics for reductive logic and proof-search. In: GALOP (Games for Logic and Programming Languages), pp. 107–123 (2005)
Severi, P., Poll, E.: Pure type systems with definitions. In: Matiyasevich, Y.V., Nerode, A. (eds.) LFCS 1994. LNCS, vol. 813, pp. 316–328. Springer, Heidelberg (1994)
Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. Theoretical Computer Science 342(1), 28–55 (2005)
Schöpp, U., Stark, I.: A Dependent Type Theory with Names and Binding. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 235–249. Springer, Heidelberg (2004)
Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theoretical Computer Science 323(1–3), 473–497 (2004)
Urzyczyn, P., Sørensen, M.: Lectures on the Curry-Howard isomorphism. Studies in Logic, vol. 149. Elsevier, Amsterdam (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gabbay, M.J., Mulligan, D.P. (2008). One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations. In: Hodges, W., de Queiroz, R. (eds) Logic, Language, Information and Computation. WoLLIC 2008. Lecture Notes in Computer Science(), vol 5110. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69937-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-69937-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69936-1
Online ISBN: 978-3-540-69937-8
eBook Packages: Computer ScienceComputer Science (R0)