Hybrid Transactional and Analytical Processing (HTAP) databases require processing transactional and analytical queries in isolation to remove the interference between them. To achieve this, it is necessary to maintain different replicas of data specified for the two types of queries. However, it is challenging to provide a consistent view for distributed replicas within a storage system, where analytical requests can efficiently read consistent and fresh data from transactional workloads at scale and with high availability. To meet this challenge, we propose extending replicated state machine-based consensus algorithms to provide consistent replicas for HTAP workloads. Based on this novel idea, we present a Raft-based HTAP database: TiDB. In the database, we design a multi-Raft storage system which consists of a row store and a column store. The row store is built based on the Raft algorithm. It is scalable to materialize updates from transactional requests with high availability. In particular, it asynchronously replicates Raft logs to learners which transform row format to column format for tuples, forming a real-time updatable column store. This column store allows analytical queries to efficiently read fresh and consistent data with strong isolation from transactions on the row store. Based on this storage system, we build an SQL engine to process large-scale distributed transactions and expensive analytical queries. The SQL engine optimally accesses row-format and column-format replicas of data. We also include a powerful analysis engine, TiSpark, to help TiDB connect to the Hadoop ecosystem. Comprehensive experiments show that TiDB achieves isolated high performance under CH-benCHmark, a benchmark focusing on HTAP workloads.

We develop a mechanized proof of Featherweight Java with Assignment and Immutability in the Coq proof assistant. This is a step towards more machine-checked proofs of a non-trivial type system. We used object immutability close to that of IGJ [9]. We describe the challenges of the mechanisation and the encoding we used inside of Coq.

Wildcard types enrich the types expressible in Java, and extend the set of typeable Java programs. Syntactic models and proofs of soundness for type systems related to Java wildcards have been suggested in the past, however, the semantics of wildcards has not yet been studied.

Tribal Ownership unifies class nesting and object ownership. Tribal Ownership is based on Tribe, a language with nested classes and object families. In Tribal Ownership, a program's runtime object ownership structure is characterised by the lexical nesting structure of its classes.We build on a variant of Tribe to present a descriptive ownership system, using object nesting to describe heap partitions, but without imposing any restrictions on programming disciplines. We then demonstrate how a range of different prescriptive ownership policies can be supported on top of the descriptive Tribal Ownership mechanism; including a novel owners-as-local-dominators policy. We formalise our type system and prove soundness and several ownership invariants. The resulting system requires strikingly few annotations, and uses well-understood encapsulation techniques to create ownership systems that should be intuitive for programmers.

Wildcards are an often confusing part of the Java type system: the behaviour of wildcard types is not fully specified by subtyping, due to wildcard capture, and the rules for type checking are often misunderstood. Their very formulation seems somehow 'different' from the rest of the Java type system, which is based on a simple, nominal hierarchy.

Existing ownership type systems require objects to have precisely one primary owner, organizing the heap into an ownership tree. Unfortunately, a tree structure is too restrictive for many programs, and prevents many common design patterns where multiple objects interact.