Modal Pure Type Systems

被引：5

作者：

Tijn Borghuis

机构：

[1] Eindhoven University of Technology,Department of Mathematics and Computing Science

来源：

Journal of Logic, Language and Information | 1998年 / 7卷 / 3期

关键词：

Knowledge representation; natural deduction; normal modal logics; typed λ-calculus;

D O I：

10.1023/A:1008254612284

中图分类号：

学科分类号：

摘要：

We present a framework for intensional reasoning in typed λ-calculus. In this family of calculi, called Modal Pure Type Systems (MPTSs), a “propositions-as-types”-interpretation can be given for normal modal logics. MPTSs are an extension of the Pure Type Systems (PTSs) of Barendregt (1992). We show that they retain the desirable meta-theoretical properties of PTSs, and briefly discuss applications in the area of knowledge representation.

引用

页码：265 / 296

页数：31

共 50 条

[31] Equality is typable in Semi-Full Pure Type Systems
Siles, Vincent
Herbelin, Hugo
25TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2010), 2010, : 21 - 30
[32] Reduction of discrete multivariable systems using pade type modal methods
Prasad, R.
Devi, S.
Journal of the Institution of Engineers (India): Electrical Engineering Division, 2001, 82 (JUNE): : 72 - 77
[33] The implicit calculus of constructions - Extending pure type systems with an intersection type binder and subtyping
Miquel, A
TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2001, 2044 : 344 - 359
[34] ON POSITIONED ECO-GRAMMAR SYSTEMS AND PURE GRAMMARS OF TYPE 0
Langer, Miroslav
Kelemenova, Alica
NEURAL NETWORK WORLD, 2013, 23 (02) : 81 - 91
[35] Embedding pure type systems in the lambda-Pi-calculus modulo
Cousineau, Denis
Dowek, Gilles
TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2007, 4583 : 102 - +
[36] Remarks on the equational theory of non-normalizing pure type systems
Barthe, G
Coquand, T
JOURNAL OF FUNCTIONAL PROGRAMMING, 2006, 16 (137-155) : 137 - 155
[37] Reviewing the classical and the de Bruijn notation for λ-calculus and pure type systems
Kamareddine, F
JOURNAL OF LOGIC AND COMPUTATION, 2001, 11 (03) : 363 - 394
[38] A first-order representation of pure type systems using superdeduction
Burel, Guillaume
TWENTY-THIRD ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2008, : 253 - 263
[39] Pure Type Systems with Corecursion on Streams From Finite to Infinitary Normalisation
Severi, Paula
de Vries, Fer-Jan
ACM SIGPLAN NOTICES, 2012, 47 (09) : 141 - 152
[40] Remarks on the equational theory of non-normalizing pure type systems
Barthe, G
Coquand, T
JOURNAL OF FUNCTIONAL PROGRAMMING, 2004, 14 : 191 - 209

← 1 2 3 4 5 →