Abstract
The modal intuitionistic epistemic logic \(\mathbf{IEL}^{-}\) was proposed by Artemov and Protopopescu as the intuitionistic version of belief logic. We construct the modal lambda calculus which is Curry-Howard isomorphic to \(\mathbf{IEL}^{-}\) as the type-theoretical representation of applicative computation widely known in functional programming.
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
Similar content being viewed by others
Notes
- 1.
In Haskell, type class is a general interface for some special group of datatypes.
References
Artemov, S., Protopopescu, T.: Intuitionistic epistemic logic. Rev. Symb. Log. 9(2), 266–298 (2016). https://doi.org/10.1017/S1755020315000374
Benton, P.N., Bierman, G.M., de Paiva, V.: Computational types from a logical perspective. J. Funct. Program. 8(2), 177–193 (1998). https://doi.org/10.1017/S0956796898002998
Goldblatt, R.I.: Grothendieck topology as geometric modality. Math. Log. Q. 27(3135), 495–529 (1981). https://doi.org/10.1002/malq.19810273104
Kakutani, Y.: Call-by-name and call-by-value in normal modal logic. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 399–414. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-76637-7_27
Kavvos, G.A.: The many worlds of modal \(\lambda \)-calculi: I. curry-howard for necessity, possibility and time. CoRR abs/1605.08106 (2016). http://arxiv.org/abs/1605.08106
Krishnaswami, N.: A computational lambda calculus for applicative functors. http://semantic-domain.blogspot.com/2012/08/a-computational-lambda-calculus-for.html
Krupski, V.N., Yatmanov, A.: Sequent calculus for intuitionistic epistemic logic IEL. In: Artemov, S., Nerode, A. (eds.) LFCS 2016. LNCS, vol. 9537, pp. 187–201. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-27683-0_14
McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1–13 (2008). https://doi.org/10.1017/S0956796807006326
Moggi, E.: Notions of computation and monads. Inform. Comput. 93(1), 55–92 (1991). https://doi.org/10.1016/0890-5401(91)90052-4. http://www.sciencedirect.com/science/article/pii/0890540191900524, selections from 1989 IEEE Symposium on Logic in Computer Science
Nederpelt, R., Geuvers, H.: Type Theory and Formal Proof: An Introduction, 1st edn. Cambridge University Press, New York (2014)
Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. 11(4), 511–540 (2001). https://doi.org/10.1017/S0960129501003322
Sorensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier Science, Amsterdam (2006)
Acknowledgment
The author is grateful to Neel Krishnaswami, Vladimir Krupski, Valerii Plisko, and Vladimir Vasyukov for consulting and advice.
The author thanks anonymous peer-reviewers for valuable and considerable comments and remarks that improved the paper significantly.
The research described in this paper was supported by Russian Foundation for Basic Research (grant 16-03-00364).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Rogozin, D. (2020). Modal Type Theory Based on the Intuitionistic Modal Logic \(\mathbf{IEL}^{-}\). In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2020. Lecture Notes in Computer Science(), vol 11972. Springer, Cham. https://doi.org/10.1007/978-3-030-36755-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-36755-8_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-36754-1
Online ISBN: 978-3-030-36755-8
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)