Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets

NOOP: A Domain-Theoretic Model of Nominally-Typed OOP

The majority of industrial-strength object-oriented (OO) software is written using nominally-typed OO programming languages. Extant domain-theoretic models of OOP developed to analyze OO type systems miss, however, a crucial feature of these mainstream OO languages: nominality. This paper presents the construction of NOOP as the first domain-theoretic model of OOP that includes full class/type names information found in nominally-typed OOP. Inclusion of nominal information in objects of NOOP and asserting that type inheritance in statically-typed OO programming languages is an inherently nomin…

A dependent nominal type theory

Nominal abstract syntax is an approach to representing names and binding pioneered by Gabbay and Pitts. So far nominal techniques have mostly been studied using classical logic or model theory, not type theory. Nominal extensions to simple, dependent and ML-like polymorphic languages have been studied, but decidability and normalization results have only been established for simple nominal type theories. We present a LF-style dependent type theory extended with name-abstraction types, prove soundness and decidability of beta-eta-equivalence checking, discuss adequacy and canonical forms via an…

Reconciling positional and nominal binding

We define an extension of the simply-typed lambda calculus where two different binding mechanisms, by position and by name, nicely coexist. In the former, as in standard lambda calculus, the matching between parameter and argument is done on a positional basis, hence alpha-equivalence holds, whereas in the latter it is done on a nominal basis. The two mechanisms also respectively correspond to static binding, where the existence and type compatibility of the argument are checked at compile-time, and dynamic binding, where they are checked at run-time.

依序排序的名义签名

Dependently Sorted Nominal Signatures

研究名义多类签名的扩展，引入广义具体化作为消去算子并构建一阶依值类系统，以表示多种演算的判断与推理规则，为形式化处理带 alpha 等价的原始表达式提供类型理论基础。

一种具有依赖类型的事件终态与终极性的演算

A dependently-typed calculus of event telicity and culminativity

本文提出一种具有依赖类型的跨语言框架，用于分析事件的终态与终极性，结合实例展示如何用该框架建模英语句子。框架分为名词域和动词域，分别处理名词短语的界限性及其与子类型、限定量词和形容词修饰的关系，以及定义依赖事件演算，区分终态事件和终极事件，并考虑副词修饰。

Typed Hilbert Epsilon Operators and the Semantics of Determiner Phrases (Invited Lecture)

The semantics of determiner phrases, be they definite de- scriptions, indefinite descriptions or quantified noun phrases, is often as- sumed to be a fully solved question: common nouns are properties, and determiners are generalised quantifiers that apply to two predicates: the property corresponding to the common noun and the one corresponding to the verb phrase. We first present a criticism of this standard view. Firstly, the semantics of determiners does not follow the syntactical structure of the sentence. Secondly the standard interpretation of the indefinite article cannot ac- count for …