arXiv subjects

Kuen-Bang Hou

Publications and source records attributed to Kuen-Bang Hou.

7 recordsLinked to original sources

arXiv2026

Technical Report: A Formal Semantics for Java Symbolic Evaluation using Large-Block Encoding

Symbolic execution plays a critical role in software reliability, as they are used to find bugs, generate test cases, and provide correctness guarantees, particularly for safety-critical systems. Yet their own correctness is rarely subject to formal scrutiny, as it is typically established empirically by evaluating tool behavior across many programs. This leaves open the possibility that the tools themselves introduce unsoundness, potentially invalidating the verification results they produce and undermining the very guarantees they are meant to provide. In this paper, we address this gap by providing the formal treatment of symbolic execution with path-merging, an optimization that improves path explosion by summarizing branching code regions into disjunctive constraints rather than exploring each path independently. Specifically, we target Java Ranger, a path-merging tool for Java programs that progressively transforms imperative Java code toward the language of formal logic through a series of code transformations. We formalize each of these transformations and prove their soundness with respect to a simplified version of the Java concrete semantics, establishing that Java Ranger's path-merging process preserves program semantics.

cs.SC↗

arXiv2026

Coslice Colimits in Homotopy Type Theory

We contribute to the theory of (homotopy) colimits inside homotopy type theory. The heart of our work characterizes the connection between (graph-indexed) colimits in a type universe and colimits in coslices of the universe, called coslice colimits. To derive this characterization, we give a construction of coslice colimits that is tailored to reveal the connection. We use the construction to prove that the forgetful functor from a coslice creates colimits over trees. We also use it to study how coslice colimits interact with orthogonal factorization systems and with cohomology theories. As a result of their interaction with orthogonal factorization systems, all colimits of pointed types preserve $n$-connectedness, which implies that higher groups, in the sense of Buchholtz, van Doorn, and Rijke, are closed under colimits. We have formalized major portions of this work (see https://github.com/PHart3/colimits-agda for the Agda code), including our main construction of the coslice colimit functor.

cs.LO↗

arXiv2020

Cellular Cohomology in Homotopy Type Theory

We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many common spaces are easier to compute. Cellular cohomology is a special kind of cohomology designed for cell complexes: these are built in stages by attaching spheres of progressively higher dimension, and cellular cohomology defines the groups out of the combinatorial description of how spheres are attached. Our main result is that for finite cell complexes, a wide class of cohomology theories (including the ones defined through Eilenberg-MacLane spaces) can be calculated via cellular cohomology. This result was formalized in the Agda proof assistant.

cs.LO↗

arXiv2018

The RedPRL Proof Assistant (Invited Paper)

RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish behavioral properties of cubical functional programs embodying the constructive content of proofs. Notably, RedPRL implements a two-level type theory, allowing an extensional, proof-irrelevant notion of exact equality to coexist with a higher-dimensional proof-relevant notion of paths.

cs.LO↗

arXiv2017

Computational Higher Type Theory III: Univalent Universes and Exact Equality

This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher-dimensional types. We extend this framework to include a cumulative hierarchy of univalent Kan universes of Kan types, exact equality and other pretypes lacking Kan structure, and a cumulative hierarchy of pretype universes. As in Parts I and II, the main result is a canonicity theorem stating that closed terms of boolean type evaluate to either true or false. This establishes the computational interpretation of Cartesian cubical higher type theory based on cubical programs equipped with a deterministic operational semantics.

cs.LO↗

arXiv2016

A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory

This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present a mechanized proof of the Blakers-Massey connectivity theorem, a result relating the higher-dimensional homotopy groups of a pushout type (roughly, a space constructed by gluing two spaces along a shared subspace) to those of the components of the pushout. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which has been studied in previous formalizations. The new proof is more elementary than existing ones in abstract homotopy-theoretic settings, and the mechanization is concise and high-level, thanks to novel combinations of ideas from homotopy theory and type theory.

cs.LO↗

arXiv2015

A Note on the Uniform Kan Condition in Nominal Cubical Sets

Bezem, Coquand, and Huber have recently given a constructively valid model of higher type theory in a category of nominal cubical sets satisfying a novel condition, called the uniform Kan condition (UKC), which generalizes the standard cubical Kan condition (as considered by, for example, Williamson in his survey of combinatorial homotopy theory) to admit phantom "additional" dimensions in open boxes. This note, which represents the authors' attempts to fill in the details of the UKC, is intended for newcomers to the field who may appreciate a more explicit formulation and development of the main ideas. The crux of the exposition is an analogue of the Yoneda Lemma for co-sieves that relates geometric open boxes bijectively to their algebraic counterparts, much as its progenitor for representables relates geometric cubes to their algebraic counterparts in a cubical set. This characterization is used to give a formulation of uniform Kan fibrations in which uniformity emerges as naturality in the additional dimensions.

math.LO↗