Searcharxiv⌕ Search

arXiv subjects

Tesla Zhang

Publications and source records attributed to Tesla Zhang.

9 recordsLinked to original sources
arXiv2025

Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols

Semantic typing has become a powerful tool for program verification, applying the technique of logical relations as not only a proof method, but also a device for prescribing program behavior. In recent work, Yao et al. scaled semantic typing to the verification of timed message-passing protocols, which are prevalent in, e.g., IoT and real-time systems applications. The appeal of semantic typing in this context is precisely because of its ability to support typed and untyped program components alike -- including physical objects -- which caters to the heterogeneity of these applications. Another demand inherent to these applications is timing: constraining the time or time window within which a message exchange must happen. Yao et al. equipped their logical relation not only with temporal predicates, but also with computable trajectories, to supply the evidence that an inhabitant can step from one time point to another one. While Yao et al. provide the formalization for such a verification tool, it lacks a mechanization. Mechanizing the system would not only provide a machine proof for it, but also facilitate scalability for future extensions and applications. This paper tackles the challenge of mechanizing the resulting proof-relevant logical relation in a proof assistant. allowing trajectories to be interleaved, partitioned, and concatenated, while the intended equality on trajectories is the equality of their graphs when seen as processes indexed by time. Unfortunately, proof assistants based on intensional type theory only have modest support for such equations, forcing a prolific use of transports. This paper reports on the process of mechanizing Yao et al.'s results, comprising the logical relation, the algebra of computable trajectories with supporting lemmas, and the fundamental theorem of the logical relation, in the Rocq theorem prover.

cs.PL↗
arXiv2025

A Language-Agnostic Logical Relation for Message-Passing Protocols

Today's computing landscape has been gradually shifting to applications targeting distributed and *heterogeneous* systems, such as cloud computing and Internet of Things (IoT) applications. These applications are predominantly *concurrent*, employ *message-passing*, and interface with *foreign objects*, ranging from externally implemented code to actual physical devices such as sensors. Verifying that the resulting systems adhere to the intended protocol of interaction is challenging -- the usual assumption of a common implementation language, let alone a type system, no longer applies, ruling out any verification method based on them. This paper develops a framework for certifying *protocol compliance* of heterogeneous message-passing systems. It contributes the first mechanization of a *language-agnostic logical relation*, asserting that its inhabitants comply with the protocol specified. This definition relies entirely on a labelled transition-based semantics, accommodating arbitrary inhabitants, typed and untyped alike, including foreign objects. As a case study, the paper considers two scenarios: (1) *per-instance verification* of a specific application or hardware device, and (2) *once-and-for-all verification* of well-typed applications for a given type system. The logical relation and both scenarios are mechanized in the Coq theorem prover.

cs.PL↗
arXiv2024

(Co)condition hits the Path

We propose an enhancement to inductive types and records in a dependent type theory, namely (co)conditions. With a primitive interval type, conditions generalize the cubical syntax of higher inductive types in homotopy type theory, while coconditions generalize the cubical path type. (Co)conditions are also useful without an interval type. The duality between conditions and coconditions is presented in an interesting way: The elimination principles of inductive types with conditions can be internalized with records with coconditions and vice versa. However, we do not develop the metatheory of conditions and coconditions in this paper. Instead, we only present the type checking.

cs.LO↗
arXiv2023

Three non-cubical applications of extension types

The development of cubical type theory inspired the idea of "extension types" which has been found to have applications in other type theories that are unrelated to homotopy type theory or cubical type theory. This article describes these applications, including on records, metaprogramming, controlling unfolding, and some more exotic ones.

cs.PL↗
arXiv2023

Two tricks to trivialize higher-indexed families

The conventional general syntax of indexed families in dependent type theories follow the style of "constructors returning a special case", as in Agda, Lean, Idris, Coq, and probably many other systems. Fording is a method to encode indexed families of this style with index-free inductive types and an identity type. There is another trick that merges interleaved higher inductive-inductive types into a single big family of types. It makes use of a small universe as the index to distinguish the original types. In this paper, we show that these two methods can trivialize some very fancy-looking indexed families with higher inductive indices (which we refer to as higher indexed families).

cs.LO↗
arXiv2022

A tutorial on implementing De Morgan cubical type theory

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 cofibration, the idea of "transportation rules" and cubical operations. This tutorial is a by-product of an experimental implementation of cubical type theory, called Guest0x0.

cs.PL↗
arXiv2021

Type theories in category theory

We introduce basic notions in category theory to type theorists, including comprehension categories, categories with attributes, contextual categories, type categories, and categories with families along with additional discussions that are not very closely related to type theories by listing definitions, lemmata (with detailed, diagram-rich proofs), and remarks. By doing so, this introduction becomes more friendly as a referential material to be read in random order (instead of from the beginning to the end). In the end, we list some mistakes made in the early versions of this introduction. The interpretation of common type formers in dependent type theories are discussed based on existing categorical constructions instead of mechanically derived from their type theoretical definition. Non-dependent type formers include unit, products (as fiber products), and functions (as fiber exponents), and dependent ones include sigma types, extensional equalities (as equalizers), pi types, and the universe of (all) propositions (as the subobject classifier).

cs.LO↗
arXiv2021

A simpler encoding of indexed types

In functional programming languages, generalized algebraic data types (GADTs) are very useful as the unnecessary pattern matching over them can be ruled out by the failure of unification of type arguments. In dependent type systems, this is usually called indexed types and it's particularly useful as the identity type is a special case of it. However, pattern matching over indexed types is very complicated as it requires term unification in general. We study a simplified version of indexed types (called simpler indexed types) where we explicitly specify the selection process of constructors, and we discuss its expressiveness, limitations, and properties.

cs.PL↗