Modal Type Theory Based on the Intuitionistic Modal Logic IEL-

被引：2

作者：

Rogozin, Daniel ^{[1
,2
]}

机构：

[1] Lomonosov Moscow State Univ, Moscow, Russia

[2] Serokell OU, Tallinn, Estonia

来源：

LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS 2020) | 2020年 / 11972卷

基金：

俄罗斯基础研究基金会;

关键词：

Intuitionistic epistemic logic; Modal type theory; Functional programming; Applicative functor;

D O I：

10.1007/978-3-030-36755-8_15

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The modal intuitionistic epistemic logic 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 IEL- as the type-theoretical representation of applicative computation widely known in functional programming.

引用

页码：236 / 248

页数：13

共 12 条

[1] INTUITIONISTIC EPISTEMIC LOGIC [J].

Artemov, Sergei ;

Protopopescu, Tudor .

REVIEW OF SYMBOLIC LOGIC, 2016, 9 (02) :266-298

[2]

Benton P. N., 1998, Journal of Functional Programming, V8, P177, DOI 10.1017/S0956796898002998

[3] GROTHENDIECK TOPOLOGY AS GEOMETRIC MODALITY [J].

GOLDBLATT, RI .

ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1981, 27 (06) :495-529

[4]

Kakutani Y, 2007, LECT NOTES COMPUT SC, V4807, P399

[5]

Kavvos G.A., 2016, ABS160508106 CORR

[6]

Krishnaswami N., A computational lambda calculus for applicative functors

[7] Sequent Calculus for Intuitionistic Epistemic Logic IEL [J].

Krupski, Vladimir N. ;

Yatmanov, Alexey .

LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS 2016), 2016, 9537 :187-201

[8] Applicative programming with effects [J].

Mcbride, Conor ;

Paterson, Ross .

JOURNAL OF FUNCTIONAL PROGRAMMING, 2008, 18 (18) :1-13

[9] NOTIONS OF COMPUTATION AND MONADS [J].

MOGGI, E .

INFORMATION AND COMPUTATION, 1991, 93 (01) :55-92

[10]

Nederpelt R, 2014, TYPE THEORY AND FORMAL PROOF: AN INTRODUCTION, P1, DOI 10.1017/CBO9781139567725

← 1 2 →