We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the semantics to be independently tailored to suit the needs of theorem proving and programming. A natural notion of irrelevancy is established where all proofs and types occurring inside programs are fully erasable without compromising their operational behavior. Through a heap-based operational semantics, we show that extracted programs always make computational progress and run memory clean without the need for runtime garbage collection. Additionally, programs can be freely lifted into the logical level for conducting deep proofs in the style of standard dependent type theories. This enables one to write resource-safe programs and verify their correctness using a unified language.

Session types provide a formal type system to define and verify communication protocols between message-passing processes. In order to analyze randomized systems, recent works have extended session types with probabilistic type constructors. Unfortunately, all the proposed extensions only support constant probabilities which limits their applicability to real-world systems. Our work addresses this limitation by introducing probabilistic refinement session types which enable symbolic reasoning for concurrent probabilistic systems in a core calculus we call PReST. The type system is carefully designed to be a conservative extension of refinement session types and supports both probabilistic and regular choice type operators. We also implement PReST in a prototype which we use for validating probabilistic concurrent programs. The added expressive power leads to significant challenges, in both the meta theory and implementation of PReST, particularly with type checking: it requires reconstructing intermediate types for channels when type checking probabilistic branching expressions. The theory handles this by semantically quantifying refinement variables in probabilistic typing rules, a deviation from standard refinement type systems. The implementation relies on a bi-directional type checker that uses an SMT solver to reconstruct the intermediate types minimizing annotation overhead and increasing usability. To guarantee that probabilistic processes are almost-surely terminating, we integrate cost analysis into our type system to obtain expected upper bounds on recursion depth. We evaluate PReST on a wide variety of benchmarks from 4 categories: (i) randomized distributed protocols such as Itai and Rodeh’s leader election, bounded retransmission, etc., (ii) parametric Markov chains such as random walks, (iii) probabilistic analysis of concurrent data structures such as queues, and (iv) distributions obtained by composing uniform distributions using operators like max and sum. Our experiments show that the PReST type checker scales to large programs with sophisticated probabilistic distributions.

Learning-based surface reconstruction methods have received considerable attention in recent years due to their excellent expressiveness. However, existing learning-based methods lack scalability in processing large-scale point clouds. This paper proposes a novel scalable learning-based 3D surface reconstruction method based on octree, called SSRNet. SSRNet works in a scalable reconstruction pipeline, which divides oriented point clouds into different local parts and then processes them in parallel. Accommodating this scalable design pattern, SSRNet constructs local geometric features for octree vertices. Such features comprise the relation between the vertices and the implicit surface, ensuring geometric perception. Focusing on local geometric information also enables the network to avoid the overfitting problem and generalize well on different datasets. Finally, as a learning-based method, SSRNet can process large-scale point clouds in a short time. And to further solve the efficiency problem, we provide a lightweight and efficient version that is about five times faster while maintaining reconstruction performance. Experiments show that our methods achieve state-of-the-art performance with outstanding efficiency.

Recently, neural implicit surfaces learning by volume rendering has become popular for multi-view reconstruction. However, one key challenge remains: existing approaches lack explicit multi-view geometry constraints, hence usually fail to generate geometry-consistent surface reconstruction. To address this challenge, we propose geometry-consistent neural implicit surfaces learning for multi-view reconstruction. We theoretically analyze that there exists a gap between the volume rendering integral and point-based signed distance function (SDF) modeling. To bridge this gap, we directly locate the zero-level set of SDF networks and explicitly perform multi-view geometry optimization by leveraging the sparse geometry from structure from motion (SFM) and photometric consistency in multi-view stereo. This makes our SDF optimization unbiased and allows the multi-view geometry constraints to focus on the true surface optimization. Extensive experiments show that our proposed method achieves high-quality surface reconstruction in both complex thin structures and large smooth regions, thus outperforming the state-of-the-arts by a large margin.