Abstract
We set out to find something that corresponds to deep inference in the same way that the lambda-calculus corresponds to natural deduction. Starting from natural deduction for the conjunction-implication fragment of intuitionistic logic we design a corresponding deep inference system together with reduction rules on proofs that allow a fine-grained simulation of beta-reduction.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Brünnler, K., Lengrand, S.: On two forms of bureaucracy in derivations. In: Bruscoli, P., Lamarche, F., Stewart, C. (eds.) Structures and Deduction, pp. 69–80. Technische Universität Dresden (2005)
Curien, P.-L.: Categorical Combinators, Sequential Algorithms and Functional Programming, 2nd edn. Research Notes in Theoretical Computer Science. Birkhäuser, Basel (1993)
de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings) 75(5), 381–392 (1972)
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1990)
Guglielmi, A.: A system of interaction and structure. ACM Transactions on Computational Logic 8(1), 1–64 (2007)
Guglielmi, A., Gundersen, T.: Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science 4(1:9), 1–36 (2008), http://arxiv.org/pdf/0709.1205
Hardin, T.: From categorical combinators to λσ-calculi, a quest for confluence. Technical report, INRIA Rocquencourt (1992), http://hal.inria.fr/inria-00077017/
Lambek, J., Scott, P.J.: Introduction to higher order categorical logic. Cambridge University Press, New York (1986)
Mac Lane, S.: Categories for the Working Mathematician. In: Graduate Texts in Mathematics. Springer, Heidelberg (1971)
Parigot, M.: λμ-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624. Springer, Heidelberg (1992)
Tiu, A.F.: A local system for intuitionistic logic. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol. 4246, pp. 242–256. Springer, Heidelberg (2006), http://users.rsise.anu.edu.au/~tiu/localint.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brünnler, K., McKinley, R. (2008). An Algorithmic Interpretation of a Deep Inference System. In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-89439-1_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89438-4
Online ISBN: 978-3-540-89439-1
eBook Packages: Computer ScienceComputer Science (R0)