首页> 美国政府科技报告 >An Interpretation of Martin-Loef's Type Theory in a Type Free Theory of Propositions

【24h】

An Interpretation of Martin-Loef's Type Theory in a Type Free Theory of Propositions

机译：解释马丁 - 洛夫在一类自由命题理论中的类型理论

获取原文

页面导航

摘要
著录项
相似文献
相关主题

摘要

A formal theory of propositions and combinator terms is presented with Frege structures as models. The basic notions of the theory are propositions and true proppositions formed by means of logical operations. The interpretation of the type theory within the logical theory is based on the semantical explanation of the type theory given by Martin-Loef excluding the type of well orderings. Intuition leading to logical theory is taken from Aczel. The construction of the interpretation can also be viewed as a formalized realizability interpretation.

著录项

作者
Smith, J.;
展开▼
作者单位

展开▼
年度 1980
页码 p.1-40
总页数 40
原文格式 PDF
正文语种 eng
中图分类工业技术;
关键词
Mathematical logic; Number theory; Set theory; Boolean algebra; Philosophy; Semantics; Theorem proving;

机译：数学逻辑;数论;集合论;布尔代数;哲学;语义学;定理证明;

相似文献

外文文献
中文文献
专利

1. The biequivalence of locally cartesian closed categories and Martin-Loef type theories [J] . PIERRE CLAIRAMBAULT, PETER DYBJER Mathematical structures in computer science . 2014,第6期

机译：局部笛卡尔封闭类别与Martin-Loef类型理论的双等价性
2. Modeling Martin-Loef type theory in categories [J] . Francois Lamarche Journal of Applied Logic . 2014,第1期

机译：在类别中建模Martin-Loef类型理论
3. Interpretation of Constructive Multi-Typed Theory in the Theory of Arithmetical Truth [J] . F. Kachapova Lobachevskii journal of mathematics . 2015,第4期

机译：算术真理理论对建构性多类型理论的解释
4. A Type-Checking Algorithm for Martin-Loef Type Theory with Subtyping Based on Normalisation by Evaluation [C] . Daniel Fridlender, Miguel Pagano Typed lambda calculi and applications . 2013

机译：基于评估归一化的Martin-Loef子类型理论的子类型检查算法
5. The well role ideal type theory: A companion to Parsons sick role ideal type in the social system. [D] . Werner, Thomas Paul. 2009

机译：良好角色理想类型理论：社会系统中帕森斯病态理想类型的伴侣。
6. Charge Transfer Enhancement in the D-π-A Type Porphyrin Dyes: A Density Functional Theory (DFT) and Time-Dependent Density Functional Theory (TD-DFT) Study [O] . Guo-Jun Kang, Chao Song, Xue-Feng Ren 2016

机译：D-π-A型卟啉染料中电荷转移的增强：密度泛函理论（DFT）和时变密度泛函理论（TD-DFT）的研究
7. A cartesian closed category in Martin-Loef's intuitionistic type theory [O] . VALENTINI S. 2003

机译：Martin-Loef直觉类型理论中的笛卡尔封闭类别
8. Relationship between the Subset and Sigma Types in Martin-Loef's '79 Type Theory [R] . Chisholm, P. 1988

机译：martin-Loef'79型理论中子集与sigma类型的关系

An Interpretation of Martin-Loef's Type Theory in a Type Free Theory of Propositions

摘要

著录项

相似文献

相关主题

期刊订阅