Type-safe casting

Many modern extensible systems, such as Java and the SPIN operating system, depend on type safety for memory protection. Unfortunately, current type-safe languages do not support systems programming well, because they do not give programmers the ability to deal with untyped data easily. In particular, they do not support the ability to cast between untyped data and language-level types. We describe a powerful, type-safe cast operator that helps programmers write low-level systems codes in type-safe languages. We have implemented this operator in Modula-3 for the SPIN operating system, and we give specific examples of how we use it in SPIN. © 1998 John Wiley & Sons, Ltd.     

Emerald: A general-purpose programming language

Emerald is a general-purpose language with aspects of traditional object-oriented languages, such as Smalltalk, and abstract data type languages, such as Modula-2 and Ada. It is strongly typed with a non-traditional object model and type system that emphasize abstract types, allow separation of typing and implementation, and provide the flexibility of polymorphism and subtyping with compile-time checking. This paper describes the Emerald language and its programming methodology. We give examples that demonstrate Emerald's features, and compare and contrast the Emerald approach to programming with the approaches used in other similar languages.     

Integrated implementation of dynamic untyped object‐based operator overloading

Operator overloading, a popular mechanism in the C++ language, is a form of ad hoc polymorphism on operator functions, allowing alternative implementations for different argument types. Classless languages with untyped objects are languages that lack classes and treat all objects as compliant to a common Object type. Languages in this category are flexible, dynamic, and easy‐to‐use, with popular examples being JavaScript, Lua, and ActionScript (the latter being hybrid by also offering classes). This paper presents an integrated implementation of untyped operator overloading which enable users to handle dynamically the full range of operators on objects. The focus is on features not supported by other languages, such as (i) arithmetic and relational operators allowing to separately handle caller lhs and rhs positions; (ii) an assignment operator with an untyped analogy of type casting; (iii) a slot access operator allowing user‐defined policies for editing object slots; and (iv) a function‐call operator to support functors. Operators are treated as first‐class object slots, distinguished by reserved indices that match the respective operator lexemes. All reported techniques have been applied in implementing the operator overloading features of the Delta language. Copyright © 2010 John Wiley & Sons, Ltd.     

Heap-Bounded Assembly Language

We present a first-order linearly typed assembly language, HBAL, that allows the safe reuse of heap space for elements of different types. Linear typing ensures the single pointer property, disallowing aliasing but allowing safe, in-place-update compilation of programming languages. We prove that HBAL is sound for a low-level untyped model of the machine, using a satisfiability relation that captures when a location correctly models a value of some type. This interpretation is closer to the machine than previous abstract machines used for typed assembly language models, and we separate typing of the store from an untyped operational semantics of programs, as would be required for proof-carrying code. Our ultimate aim is to design a family of assembly languages that have high-level typing features for expressing resource-bound constraints. We want to link the assembly-level with high-level languages expressing similar constraints, to provide end-to-end guarantees and a viable framework for proof-carrying code. HBAL is a first exemplifying step in this direction. It is designed as a target low-level language for Hofmann's LFPL language. Programs written in LFPL run in a bounded amount of heap space, and this property carries over when they are compiled to HBAL: the resulting program does not allocate store or assume an external garbage collector. Following LFPL, we include a special diamond resource type that stands for a unit of heap space of uncommitted type.     

On regular realizability problems for context-free languages

We consider regular realizability problems, which consist in verifying whether the intersection of a regular language which is the problem input and a fixed language (filter) which is a parameter of the problem is nonempty. We study the algorithmic complexity of regular realizability problems for context-free filters. This characteristic is consistent with the rational dominance relation of CF languages. However, as we prove, it is more rough. We also give examples of both P-complete and NL-complete regular realizability problems for CF filters. Furthermore, we give an example of a subclass of CF languages for filters of which the regular realizability problems can have an intermediate complexity. These are languages with polynomially bounded rational indices.     

Definition,mathematical examples and quantum chemical applications of nested summation symbols and logical Kronecker deltas

Two mathematical symbols are introduced and their applications to computational chemistry and to artificial intelligence are described. The first symbol is called a nested summation symbol (NSS). After a discussion of its properties, we insist on the significance of this symbol in developing sequential and parallel computational algorithms. Another group of symbols, related to logical expressions, are defined under the name logical Kronecker deltas (LKDs). Application examples of the NSS and LKD technique to several computational quantum chemistry topics are given. It is shown how some standard formulae become shorter and easier to write, generalize, program and evaluate. It is emphasized that both symbols constitute a powerful link between mathematical formalism and programming in high level languages.     

Ontology oriented programming in go!

In this paper we introduce the knowledge representation features of a new multi-paradigm programming language called go! that cleanly integrates logic, functional, object oriented and imperative programming styles. Borrowing from L&O [1] go! allows knowledge to be represented as a set of labeled theories incrementally constructed using multiple-inheritance. The theory label is a constructor for instances of the class. The instances are go!’s objects. A go! theory structure can be used to characterize any knowledge domain. In particular, it can be used to describe classes of things, such as people, students, etc., their subclass relationships and characteristics of their key properties. That is, it can be used to represent an ontology. For each ontology class we give a type definition—we declare what properties, with what value type, instances of the class have—and we give a labeled theory that defines these properties. Subclass relationships are reflected using both type and theory inheritance rules. Following [2], we shall call this ontology oriented programming. This paper describes the go! language and its use for ontology oriented programming, comparing its expressiveness with Owl, particularly Owl Lite[3]. The paper assumes some familiarity with ontology specification using Owl like languages and with logic and object oriented programming.     

An approach to high-level language bindings to XML

Values of existing typed programming languages are increasingly generated and manipulated outside the language jurisdiction. Instead, they often occur as fragments of XML documents, where they are uniformly interpreted as labelled trees in spite of their domain-specific semantics. In particular, the values are divorced from the high-level type with which they are conveniently, safely, and efficiently manipulated within the language.We propose language-specific mechanisms which extract language values from arbitrary XML documents and inject them in the language. In particular, we provide a general framework for the formal interpretation of extraction mechanisms and then instantiate it to the definition of a mechanism for a sample language core L. We prove that such mechanism can be built by giving a sound and complete algorithm that implements it.The values, types, and type semantics of L are sufficiently general to show that extraction mechanisms can be defined for many existing typed languages, including object-oriented languages. In fact, extraction mechanisms for a large class of existing languages can be directly derived from L's. As a proof of this, we introduce the SNAQue prototype system, which transforms XML fragments into CORBA objects and exposes them across the ORB framework to any CORBA-compliant language.     

On regular realizability problems

We consider the class of regular realizability problems. Any of such problems is specified by some language (filter) and consists in verifying that the intersection of a given regular language and the filter is nonempty. The main question is diversity of the computational complexity of such problems. We show that any regular realizability problem with an infinite filter is hard for a class of problems decidable in logarithmic space with respect to logarithmic reductions. We give examples of NP-complete and PSPACE-complete regular realizability problems.     

Strongly Typed Term Representations in Coq

There are two approaches to formalizing the syntax of typed object languages in a proof assistant or programming language. The extrinsic approach is to first define a type that encodes untyped object expressions and then make a separate definition of typing judgements over the untyped terms. The intrinsic approach is to make a single definition that captures well-typed object expressions, so ill-typed expressions cannot even be expressed. Intrinsic encodings are attractive and naturally enforce the requirement that metalanguage operations on object expressions, such as substitution, respect object types. The price is that the metalanguage types of intrinsic encodings and operations involve non-trivial dependency, adding significant complexity. This paper describes intrinsic-style formalizations of both simply-typed and polymorphic languages, and basic syntactic operations thereon, in the Coq proof assistant. The Coq types encoding object-level variables (de Bruijn indices) and terms are indexed by both type and typing environment. One key construction is the boot-strapping of definitions and lemmas about the action of substitutions in terms of similar ones for a simpler notion of renamings. In the simply-typed case, this yields definitions that are free of any use of type equality coercions. In the polymorphic case, some substitution operations do still require type coercions, which we at least partially tame by uniform use of heterogeneous equality.     

Effective strategic programming for Java developers

In object programming languages, the Visitor design pattern allows separation of algorithms and data structures. When applying this pattern to tree‐like structures, programmers are always confronted with the difficulty of making their code evolve. One reason is that the code implementing the algorithm is interwound with the code implementing the traversal inside the visitor. When implementing algorithms such as data analyses or transformations, encoding the traversal directly into the algorithm turns out to be cumbersome as this type of algorithm only focuses on a small part of the data‐structure model (e.g., program optimization). Unfortunately, typed programming languages like Java do not offer simple solutions for expressing generic traversals. Rewrite‐based languages like ELAN or Stratego have introduced the notion of strategies to express both generic traversal and rule application control in a declarative way. Starting from this approach, our goal was to make the notion of strategic programming available in a widely used language such as Java and thus to offer generic traversals in typed Java structures. In this paper, we present the strategy language SL that provides programming support for strategies in Java. Copyright © 2012 John Wiley & Sons, Ltd.     

Type-directed weaving of aspects for polymorphically typed functional languages

Incorporating aspect-oriented paradigm to a polymorphically typed functional language enables the declaration of type-scoped advice, in which the effect of an aspect can be harnessed by introducing possibly polymorphic type constraints to the aspect. The amalgamation of aspect orientation and functional programming enables quick behavioral adaption of functions, clear separation of concerns and expressive type-directed programming. However, proper static weaving of aspects in polymorphic languages with a type-erasure semantics remains a challenge. In this paper, we describe a type-directed static weaving strategy, as well as its implementation, that supports static type inference and static weaving of programs written in an aspect-oriented polymorphically typed functional language, AspectFun. We show examples of type-scoped advice, identify the challenges faced with compile-time weaving in the presence of type-scoped advice, and demonstrate how various advanced aspect features can be handled by our techniques. Finally, we prove the correctness of the static weaving strategy with respect to the operational semantics of AspectFun.     

Relational Interpretations of Recursive Types in an Operational Setting

Relational interpretations of type systems are useful for establishing properties of programming languages. For languages with recursive types it is difficult to establish the existence of a relational interpretation. The usual approach is to pass to a domain-theoretic model of the language and, exploiting the structure of the model, to derive relational properties of it. We investigate the construction of relational interpretations of recursive types in a purely operational setting, drawing on recent ideas from domain theory and operational semantics as a guide. We prove syntactic minimal invariance for an extension of PCF with a recursive type, a syntactic analogue of the minimal invariance property used by Freyd and Pitts to characterize the domain interpretation of a recursive type. As Pitts has shown in the setting of domains, syntactic minimal invariance suffices to establish the existence of relational interpretations. We give two applications of this construction. First, we derive a notion of logical equivalence for expressions of the language that we show coincides with experimental equivalence and which, by virtue of its construction, validates useful induction and coinduction principles for reasoning about the recursive type. Second, we give a relational proof of correctness of the continuation-passing transformation, which is used in some compilers for functional languages.     

On Semidefinite Programming Relaxations of (2+p)-SAT

Recently, de Klerk, van Maaren and Warners [10] investigated a relaxation of 3-SAT via semidefinite programming. Thus a 3-SAT formula is relaxed to a semidefinite feasibility problem. If the feasibility problem is infeasible then a certificate of unsatisfiability of the formula is obtained. The authors proved that this approach is exact for several polynomially solvable classes of logical formulae, including 2-SAT, pigeonhole formulae and mutilated chessboard formulae. In this paper we further explore this approach, and investigate the strength of the relaxation on (2+p)-SAT formulae, i.e., formulae with a fraction p of 3-clauses and a fraction (1–p) of 2-clauses. In the first instance, we provide an empirical computational evaluation of our approach. Secondly, we establish approximation guarantees of randomized and deterministic rounding schemes when the semidefinite feasibility problem is feasible, and also present computational results for the rounding schemes. In particular, we do a numerical and theoretical comparison of this relaxation and the stronger relaxation by Karloff and Zwick [15].     

Intersection Typed λ-calculus

The aim of this paper is to discuss the design of an explicitly typed λ-calculus corresponding to the Intersection Type Assignment System (IT) which assigns intersection types to the untyped λ-calculus. Two different proposals are given. The logical foundation of all of them is the Intersection Logic IL.     

逻辑型语言和过程型语言中的COM技术

本文探讨了在过程型程序设计语言与逻缉型程序设计语言中COM(Component 0bject Model)技术的实现方法，从而改变了以往用这两类语言编写的程序之间的松耦合关系，实现了两类不同种类语言之间的无缝连接，使它们能在深层次上自由地进行信息交流．本文还以Visual C 和Visual．Prolog为例，给出了一些有参考价值的实例．     

A theory of type polymorphism in programming

The aim of this work is largely a practical one. A widely employed style of programming, particularly in structure-processing languages which impose no discipline of types, entails defining procedures which work well on objects of a wide variety. We present a formal type discipline for such polymorphic procedures in the context of a simple programming language, and a compile time type-checking algorithm $\text{W}$ which enforces the discipline. A Semantic Soundness Theorem (based on a formal semantics for the language) states that well-type programs cannot “go wrong” and a Syntactic Soundness Theorem states that if $\text{W}$ accepts a program then it is well typed. We also discuss extending these results to richer languages; a type-checking algorithm based on $\text{W}$ is in fact already implemented and working, for the metalanguage ML in the Edinburgh LCF system.     

LMNtal as a hierarchical logic programming language

LMNtal (pronounced “elemental”) is a simple language model based on hierarchical graph rewriting that uses logical variables to represent connectivity and membranes to represent hierarchy. LMNtal is an outcome of the attempt to unify constraint-based concurrency and Constraint Handling Rules (CHR), the two notable extensions to concurrent logic programming. LMNtal is intended to be a substrate language of various computational models, especially those addressing concurrency, mobility and multiset rewriting. Although the principal objective of LMNtal was to provide a unifying computational model, it is of interest to equip the formalism with a precise logical interpretation. In this paper, we show that it is possible to give LMNtal a simple logical interpretation based on intuitionistic linear logic and a flattening technique. This enables us to call LMNtal a hierarchical, concurrent linear logic language.     

The Green language type system

A programming language that considers basic values and classes as objects brings more opportunities of code reuse and it is easier to use than a language that does not support this feature. However, popular statically typed object-oriented languages do not consider classes as first-class objects because this concept is difficult to integrate with static type checking. They also do not consider basic values as objects for sake of efficiency. This article presents the Green language type system which supports classes as classless objects and offers a mechanism to treat basic values as objects. The result is a reasonably simple type system which is statically typed and easy to implement. It simplifies several other language mechanisms and prevents any infinite regression of metaclasses.