1997
Typed logics with states
Publication
Publication
The paper presents a simple format for typed logics with states by adding a function for register update to standard typed lambda calculus. It is shown that universal validity of equality for this extended language is decidable (extending a well-known result of Friedman for typed lambda calculus). This system is next extended to a full fledged typed dynamic logic, and it is illustrated how the resulting format allows for very simple and intuitive representations of dynamic semantics for natural language and denotational semantics for imperative programming. The proposal is compared with some alternative approaches to formulating typed versions of dynamic logics.
| Additional Metadata | |
|---|---|
| Language Constructs and Features (acm D.3.3), Semantics of Programming Languages (acm F.3.2), Knowledge Representation Formalisms and Methods (acm I.2.4), Natural Language Processing (acm I.2.7) | |
| Higher-order logic and type theory (msc 03B15), Logic of natural languages (msc 03B65), Logic in computer science (msc 03B70), Semantics (msc 68Q55), Abstract data types; algebraic specification (msc 68Q65) | |
| CWI | |
| Information Systems [INS] | |
| Organisation | Standardization and Knowledge Transfer |
|
van Eijck, D.J.N. (1997). Typed logics with states. Information Systems [INS]. CWI.
|
|
