相关论文: A circular version of G\"odel's T and its abstract…
We introduce a simple extension of the $\lambda$-calculus with pairs---called the distributive $\lambda$-calculus---obtained by adding a computational interpretation of the valid distributivity isomorphism $A \Rightarrow (B\wedge C)\ \…
This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types equipped with higher-order primitive…
Guarded recursion is a powerful modal approach to recursion that can be seen as an abstract form of step-indexing. It is currently used extensively in separation logic to model programming languages with advanced features by solving domain…
A coarse description of a subset A of omega is a subset D of omega such that the symmetric difference of A and D has asymptotic density 0. We study the extent to which noncomputable information can be effectively recovered from all coarse…
This paper is a continuation of our 2005 paper on complex topology and its implication on invertibility (or non-invertibility). In this paper, we will try to classify the complexity of inversion into 3 different classes. We will use…
We discuss here constraint programming (CP) by using a proof-theoretic perspective. To this end we identify three levels of abstraction. Each level sheds light on the essence of CP. In particular, the highest level allows us to bring CP…
In this paper we develop cyclic proof systems for the problem of inclusion between the least sets of models of mutually recursive predicates, when the ground constraints in the inductive definitions belong to the quantifier-free fragments…
Cluster-tilted algebras are trivial extensions of tilted algebras. This correspondence induces a surjective map from tilted algebras to cluster-tilted algebras. If B is a cluster-tilted algebra, we use the fibre of B under this map to study…
This paper provides a general account of the notion of recursive program schemes, studying both uninterpreted and interpreted solutions. It can be regarded as the category-theoretic version of the classical area of algebraic semantics. The…
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract…
We study the computational expressivity of proof systems with fixed point operators, within the 'proofs-as-programs' paradigm. We start with a calculus muLJ (due to Clairambault) that extends intuitionistic logic by least and greatest…
Two novel descriptions of weak {\omega}-categories have been recently proposed, using type-theoretic ideas. The first one is the dependent type theory CaTT whose models are {\omega}-categories. The second is a recursive description of a…
We present a sequent-style proof system for provability logic GL that admits so-called circular proofs. For these proofs, the graph underlying a proof is not a finite tree but is allowed to contain cycles. As an application, we establish…
In Monoidal Computer I, we introduced a categorical model of computation where the formal reasoning about computability was supported by the simple and popular diagrammatic language of string diagrams. In the present paper, we refine and…
We classify compact surfaces with torsion-free affine connections for which every geodesic is a simple closed curve. In the process, we obtain completely new proofs of all the major results concerning the Riemannian case. In contrast to…
We show the problem of counting homomorphisms from the fundamental group of a homology $3$-sphere $M$ to a finite, non-abelian simple group $G$ is #P-complete, in the case that $G$ is fixed and $M$ is the computational input. Similarly,…
The authors' ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs run in type-2 polynomial-time and all standard type-2 basic feasible functionals are ATR-definable…
Explanations of cognitive behavior often appeal to computations over representations. What does it take for a system to implement a given computation over suitable representational vehicles within that system? We argue that the language of…
A central method for analyzing the asymptotic complexity of a functional program is to extract and then solve a recurrence that expresses evaluation cost in terms of input size. The relevant notion of input size is often specific to a…
Towards better understanding of gate elimination, the only method known that can prove complexity lower bounds for explicit functions against unrestricted Boolean circuits, this work contributes: (1) formalizing circuit simplifications as a…