17 citations · 55 across the 16 of their papers we have counts for
12 papers · 1 filter
On the complexity of normalization for the planar -calculus
Anupam Das, Damiano Mazza, Lê Thành Dũng Nguyên +1
We sketch a tentative proof of P-completeness for the -convertibility problem on untyped planar (a.k.a. ordered or non-commutative) -terms.
Proof Theory of Partially Normal Skew Monoidal Categories
Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
The skew monoidal categories of Szlachányi are a weakening of monoidal categories where the three structural laws of left and right unitality and associativity are not required to…
Deductive Systems and Coherence for Skew Prounital Closed Categories
Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
In this paper, we develop the proof theory of skew prounital closed categories. These are variants of the skew closed categories of Street where the unit is not represented. Skew c…
The Sequent Calculus of Skew Monoidal Categories
Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
Szlachányi's skew monoidal categories are a well-motivated variation of monoidal categories in which the unitors and associator are not required to be natural isomorphisms, but mer…
A theory of linear typings as flows on 3-valent graphs
Noam Zeilberger
Building on recently established enumerative connections between lambda calculus and the theory of embedded graphs (or "maps"), this paper develops an analogy between typing (of la…
A sequent calculus for the Tamari order
Noam Zeilberger
We introduce a sequent calculus with a simple restriction of Lambek's product rules that precisely captures the classical Tamari order, i.e., the partial order on fully-bracketed w…
A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine
Paul-André Melliès, Noam Zeilberger
Combining insights from the study of type refinement systems and of monoidal closed chiralities, we show how to reconstruct Lawvere's hyperdoctrine of presheaves using a full and f…
Linear lambda terms as invariants of rooted trivalent maps
Noam Zeilberger
The main aim of the article is to give a simple and conceptual account for the correspondence (originally described by Bodini, Gardy, and Jacquot) between -equivalence classes o…
Counting isomorphism classes of -normal linear lambda terms
Noam Zeilberger
Unanticipated connections between different fragments of lambda calculus and different families of embedded graphs (a.k.a. "maps") motivate the problem of enumerating -normal li…
An Isbell Duality Theorem for Type Refinement Systems
Paul-André Melliès, Noam Zeilberger
Any refinement system (= functor) has a fully faithful representation in the refinement system of presheaves, by interpreting types as relative slice categories, and refinement typ…
A correspondence between rooted planar maps and normal planar lambda terms
Noam Zeilberger, Alain Giorgetti
A rooted planar map is a connected graph embedded in the 2-sphere, with one edge marked and assigned an orientation. A term of the pure lambda calculus is said to be linear if ever…
Type refinement and monoidal closed bifibrations
Paul-André Melliès, Noam Zeilberger
The concept of_refinement_ in type theory is a way of reconciling the "intrinsic" and the "extrinsic" meanings of types. We begin with a rigorous analysis of this concept, settling…