Related papers: Java Generics are Turing Complete

Grigore showed that Java generics are Turing complete by describing a reduction from Turing machines to Java subtyping. We apply Grigore's algorithm to Python type hints and deduce that they are Turing complete. In addition, we present an…

Parser generators generate translators from language specifications. In many cases, such specifications contain semantic actions written in the same language as the generated code. Since these actions are subject to little static checking,…

Extending a given language with new dedicated features is a general and quite used approach to make the programming language more adapted to problems. Being closer to the application, this leads to less programming flaws and easier…

Java's type system mostly relies on type checking augmented with local type inference to improve programmer convenience. We study global type inference for Featherweight Generic Java (FGJ), a functional Java core language. Given generic…

JDBC remains a key technology for database access in Java applications. Since the database dictionary and the Java type system have distinct scopes, developers inevitably need to deal with bugs in SQL-to-Java type mappings. We propose an…

The mathematical modeling of generics in Java and other similar nominally-typed object-oriented programming languages is a challenge. In this short paper we present the outline of a novel order-theoretic approach to modeling generics, in…

Generics have been added to Java so as to increase the expressiveness of its type system. Generics in Java, however, include some features---such as Java wildcards, $F$-bounded generics, and Java erasure---that have been hard to analyze and…

Pluggable type systems allow programmers to extend the type system of a programming language to enforce semantic properties defined by the programmer. Pluggable type systems are difficult to deploy in legacy codebases because they require…

We demonstrate a method to infer polymorphically principal and subtyping-minimal types for an ML-like core language by assigning ranges within a lattice to type variables. We demonstrate the termination and completeness of this algorithm,…

We prove that Cypher 25, the graph query language of Neo4j, is Turing-complete. The proof shows that a single RETURN statement using reduce(), CASE expressions, and list comprehensions can simulate any 2-counter machine (Minsky 1967). We…

This paper presents a technique for deadlock detection of Java programs. The technique uses typing rules for extracting infinite-state abstract models of the dependencies among the components of the Java intermediate language -- the Java…

We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is…

Of the complex features of generic nominally-typed OO type systems, wildcard types and variance annotations are probably the hardest to fully grasp. As demonstrated when adding closures (a.k.a., lambdas) and when extending type inference in…

This paper addresses compositional and incremental type checking for object-oriented programming languages. Recent work achieved incremental type checking for structurally typed functional languages through co-contextual typing rules, a…

Bugs that are detected earlier during the development lifecycle are easier and cheaper to fix, whereas bugs that are found during production are difficult and expensive to address, and may have dire consequences. Type systems are…

Reflective systems allow their own structures to be altered from within. Here we are concerned with a style of reflection, called linguistic reflection, which is the ability of a running program to generate new program fragments and to…

We position Turing's result regarding the undecidability of the halting problem as a result about programs rather than machines. The mere requirement that a program of a certain kind must solve the halting problem for all programs of that…

A reasonable C++ Java Native Interface (JNI) technique termed C++ Wrappered JNI (C++WJ) is presented. The technique simplifies current error-prone JNI development by wrappering JNI calls. Provided development is done with the aid of a C++…

Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of…

Code completion is a key feature of Integrated Development Environments (IDEs), aimed at predicting the next tokens a developer is likely to write, helping them write code faster and with less effort. Modern code completion approaches are…