Related papers: Constructing the Propositional Truncation using No…
A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations,…
We prove that the half plane version of the uniform infinite planar triangulation (UIPT) is recurrent. The key ingredients of the proof are a construction of a new full plane extension of the half plane UIPT, based on a natural…
This paper presents a new type analysis for logic programs. The analysis is performed with a priori type definitions; and type expressions are formed from a fixed alphabet of type constructors. Non-discriminative union is used to join type…
This paper develops a novel nested sequent proof-search methodology for intuitionistic tense logics (ITLs), supporting finite counter-model extraction. We introduce a new loop-checking method that detects repeating nested sequents using…
We introduce the notion of homotopically discrete n-fold category as an n-fold generalization of a groupoid with no non-trivial loops. We give two equivalent descriptions of this structure: in terms of a Segal-type model and in terms of…
Several authors devised type-based termination criteria for ML-like languages allowing non-structural recursive calls. We extend these works to general rewriting and dependent types, hence providing a powerful termination criterion for the…
We introduce a sequent calculus for the propositional team logic with both the split disjunction and the inquisitive disjunction consisting of a Gentzen-style system (G3-like) for classical propositional logic together with two…
We construct a model category (in the sense of Quillen) for set theory, starting from two arbitrary, but natural, conventions. It is the simplest category satisfying our conventions and modelling the notions of finiteness, countability and…
We discuss different cases of dissipative Hamiltonian differential-algebraic equations and the linear algebraic systems that arise in their linearization or discretization. For each case we give examples from practical applications. An…
We provide, among other things: (i) a Bousfield--Kan formula for colimits in $\infty$-categories (generalizing the 1-categorical formula for a colimit as a coequalizer of maps between coproducts); (ii) $\infty$-categorical generalizations…
In this paper, we justify and make precise an elementary approach that establishes the existence of (co)limits in $\mathbf{Cat}$. This approach, while conceptually evident, has not been made fully explicit or systematically described in the…
We develop a novel tool to study the fixed point property of finite posets using a topological approach. Our tool is a construction which turns out to induce an endofunctor of the homotopy category of finite $T_0$--spaces. We study many…
Suppose we are given a graph and want to show a property for all its cycles (closed chains). Induction on the length of cycles does not work since sub-chains of a cycle are not necessarily closed. This paper derives a principle reminiscent…
The classical propositional logic is known to be sound and complete with respect to the set semantics that interprets connectives as set operations. The paper extends propositional language by a new binary modality that corresponds to…
We propose a new type-theoretic approach to SLD-resolution and Horn-clause logic programming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for the type given by the…
In this work we use Hodge theoretic methods to study homotopy types of complex projective manifolds with arbitrary fundamental groups. The main tool we use is the \textit{schematization functor} $X \mapsto (X\otimes \mathbb{C})^{sch}$,…
We develop synthetic notions of oracle computability and Turing reducibility in the Calculus of Inductive Constructions (CIC), the constructive type theory underlying the Coq proof assistant. As usual in synthetic approaches, we employ a…
Strongly-coupled Quantum Field Theories (QFTs) are ubiquitous in high energy physics and many-body physics, yet our ability to do precise computations in such systems remains limited. Hamiltonian Truncation is a method for doing…
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…
Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a…