An intuitionistic λ-calculus with exceptions

被引：5

作者：

David, R ^{[1
]}

Mounier, G ^{[1
]}

机构：

[1] Univ Savoie Campus Sci, Math Lab, F-733760 Le Bourget Du Lac, France

来源：

JOURNAL OF FUNCTIONAL PROGRAMMING | 2005年 / 15卷

关键词：

D O I：

10.1017/S0956796804005362

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We introduce a typed lambda-calculus which allows the use of exceptions in the ML style. It is an extension of the system AF(2) of Krivine & Leivant (Krivine, 1990; Leivant, 1983). We show its main properties: confluence, strong normalization and weak subject reduction. The system satisfies the "the proof as program" paradigm as in AF(2). Moreover, the underlined logic of our system is intuitionistic logic.

引用

页码：33 / 52

页数：20

共 50 条

[31] Sequent Calculus for Intuitionistic Epistemic Logic IEL
Krupski, Vladimir N.
Yatmanov, Alexey
LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS 2016), 2016, 9537 : 187 - 201
[32] The Lambek Calculus Extended with Intuitionistic Propositional Logic
Kaminski, Michael
Francez, Nissim
STUDIA LOGICA, 2016, 104 (05) : 1051 - 1082
[33] Intuitionistic Fuzzy Calculus Based on Einstein Operations
Guo, Changhong
Fang, Shaomei
INTERNATIONAL JOURNAL OF UNCERTAINTY FUZZINESS AND KNOWLEDGE-BASED SYSTEMS, 2021, 29 (01) : 145 - 178
[34] A Forward Unprovability Calculus for Intuitionistic Propositional Logic
Fiorentini, Camillo
Ferrari, Mauro
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2017, 2017, 10501 : 114 - 130
[35] A resource aware semantics for a focused intuitionistic calculus
Kesner, Delia
Ventura, Daniel
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2019, 29 (01) : 93 - 126
[36] Intuitionistic differential nets and lambda-calculus
Tranquilli, Paolo
THEORETICAL COMPUTER SCIENCE, 2011, 412 (20) : 1979 - 1997
[37] THE COMPLETENESS OF INTUITIONISTIC PREDICATE CALCULUS WITH THE NOTION BAR
YASHIN, AD
VESTNIK MOSKOVSKOGO UNIVERSITETA SERIYA 1 MATEMATIKA MEKHANIKA, 1984, (04): : 67 - 69
[38] SEPARATION THEOREM FOR FRAGMENTS OF INTUITIONISTIC PROPOSITIONAL CALCULUS
ROUSSEAU, G
ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1970, 16 (05): : 469 - &
[39] Neighbourhood semantics and labelled calculus for intuitionistic infinitary logic
Tesi, Matteo
Negri, Sara
JOURNAL OF LOGIC AND COMPUTATION, 2021, 31 (07) : 1608 - 1639
[40] A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic
Nomura, Shoshin
Sano, Katsuhiko
Tojo, Satoshi
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, (LPAR-20 2015), 2015, 9450 : 187 - 202

← 1 2 3 4 5 →