编程语言
This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g., concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties…
Twenty years ago, in an article titled "Covariance and contravariance: conflict without a cause", I argued that covariant and contravariant specialization of method parameters in object-oriented programming had different purposes and…
We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and type error) in a novel way, by universal properties relative to…
Theories for reasoning about programs with effects initially focused on basic manipulation of lists and other mutable data. The next challenge was to consider higher-order programming, adding functions as first class objects to mutable…
The SPARC TSO weak memory model is defined axiomatically, with a non-compositional formulation that makes modular reasoning about programs difficult. Our denotational approach uses pomsets to provide a compositional semantics capturing…
A coercion semantics of a programming language with subtyping is typically defined on typing derivations rather than on typing judgments. To avoid semantic ambiguity, such a semantics is expected to be coherent, i.e., independent of the…
Structured reversible flowchart languages is a class of imperative reversible programming languages allowing for a simple diagrammatic representation of control flow built from a limited set of control flow structures. This class includes…
To model relaxed memory, we propose confusion-free event structures over an alphabet with a justification relation. Executions are modeled by justified configurations, where every read event has a justifying write event. Justification alone…
A compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have important security benefits, as they limit the power of an…
We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and…
In order to tackle the development of concurrent and distributed systems, the active object programming model provides a high-level abstraction to program concurrent behaviours. There exists already a variety of active object frameworks…
The Internet of Things (IoT) offers the infrastructure of the information society. It hosts smart objects that automatically collect and exchange data of various kinds, directly gathered from sensors or generated by aggregations. Suitable…
Optimizing a stateful dataflow language is a challenging task. There are strict correctness constraints for preserving properties expected by downstream consumers, a large space of possible optimizations, and complex analyses that must…
We show that recent approaches of static analysis based on quantitative typing systems can be extended to programming languages with global state. More precisely, we define a call-by-value language equipped with operations to access a…
This paper presents a new synthesis-based approach for batch image processing. Unlike existing tools that can only apply global edits to the entire image, our method can apply fine-grained edits to individual objects within the image. For…
A description of language design choices that have profound effects on software quality, criticism of how ordinary OO languages address them, and explanation of the thinking behind Eiffel's corresponding mechanisms.
Capture calculus has recently been proposed as a solution to effect checking, achieved by tracking the captured references of terms in the types. Boxes, along with the box and unbox operations, are a crucial construct in capture calculus,…
This tutorial explains (one way) how to implement De Morgan cubical type theory to people who know how to implement a dependent type theory. It contains an introduction to basic concepts of cubes, type checking algorithms under a…
Qubit allocation is a process to assign physical qubits to logical qubits in a quantum program. Since some quantum computers have connectivity constraints on applications of two-qubit operations, it is mainly concerned with finding an…
Programming is an integral part of computer science discipline. Every day the programming environment is not only rapidly growing but also changing and languages are constantly evolving. Learning of object-oriented paradigm is compulsory in…