Cited By
View all- Olimpieri FGorla D(2021)Intersection type distributorsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470617(1-15)Online publication date: 29-Jun-2021
A type theory for cartesian closed bicategories
Article No.: 38, Pages 1 - 13
Abstract
We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that its syntactic model satisfies an appropriate universal property, thereby lifting the Curry-Howard-Lambek correspondence to the bicategorical setting. Our approach is principled and practical. Weak substitution structure is constructed using a bicategorification of the notion of abstract clone from universal algebra, and the rules for products and exponentials are synthesised from semantic considerations. The result is a type theory that employs a novel combination of 2-dimensional type theory and explicit substitution, and directly generalises the Simply-Typed Lambda Calculus. This work is the first step in a programme aimed at proving coherence for cartesian closed bicategories.
References
[1]
J. Bénabou, "Introduction to bicategories," in Reports of the Midwest Category Seminar. Springer Berlin Heidelberg, 1967, pp. 1--77.
[2]
R. Street, "Categorical structures," in Handbook of Algebra, M. Hazewinkel, Ed. Elsevier, 1995, vol. 1, ch. 15, pp. 529--577.
[3]
G.L. Cattani, M. Fiore, and G. Winskel, "A theory of recursive domains with applications to concurrency," in Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 1998, pp. 214--225.
[4]
S. Castellan, P. Clairambault, S. Rideau, and G. Winskel, "Games and strategies as event structures," Logical Methods in Computer Science, vol. 13, no. 3, 2017. [Online]. Available
[5]
M. G. Abbott, "Categories of containers," Ph.D. dissertation, University of Leicester, 2003.
[6]
P.-E. Dagand and C. McBride, "A categorical treatment of ornaments," in Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 2013, pp. 530--539.
[7]
M. Fiore, N. Gambino, M. Hyland, and G. Winskel, "The cartesian closed bicategory of generalised species of structures," Journal of the London Mathematical Society, vol. 77, no. 1, pp. 203--220, 2007.
[8]
N. Gambino and J. Kock, "Polynomial functors and polynomial monads," Mathematical Proceedings of the Cambridge Philosophical Society, vol. 154, no. 1, pp. 153--192, 2013.
[9]
M. Fiore and A. Joyal, "Theory of para-toposes," talk at the Category Theory 2015 Conf., Departamento de Matematica, Universidade de Aveiro, Aveiro (Portugal), 2015. [Online]. Available: http://sweet.ua.pt/dirk/ct2015/abstracts/fiore_m.pdf
[10]
N. Gambino and A. Joyal, "On operads, bimodules and analytic functors," Memoirs of the American Mathematical Society, vol. 249, no. 1184, pp. 153--192, 2017.
[11]
M. Fiore, N. Gambino, M. Hyland, and G. Winskel, "Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures," Selecta Mathematica New Series, 2017.
[12]
J. W. Gray, Formal Category Theory: Adjointness for 2-Categories, ser. Lecture Notes in Mathematics. Springer, 1974, vol. 391.
[13]
S. Mac Lane and R. Paré, "Coherence for bicategories and indexed categories," Journal of Pure and Applied Algebra, vol. 37, pp. 59--80, 1985.
[14]
A. J. Power, "Coherence for bicategories with finite bilimits I," in Categories in Computer Science and Logic: Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference Held June 14-20, 1987, J. W. Gray and A. Scedrov, Eds. American Mathematical Society, 1989, vol. 92, pp. 341--349.
[15]
P. T. Johnstone, Sketches of an Elephant. Oxford University Press, 2002.
[16]
N. Gambino and M. Hyland, "Wellfounded trees and dependent polynomial functors," in Types for Proofs and Programs, S. Berardi, M. Coppo, and F. Damiani, Eds. Springer Berlin Heidelberg, 2004, pp. 210--225.
[17]
J. Lambek, "Cartesian closed categories and typed lambda- calculi," in Proceedings of the Thirteenth Spring School of the LITP on Combinators and Functional Programming Languages. Springer-Verlag, 1986, pp. 136--175.
[18]
M. Makkai and G. Reyes, First Order Categorical Logic: Model-Theoretical Methods in the Theory of Topoi and Related Categories. Springer, 1977.
[19]
A. Church, "A formulation of the simple theory of types," The Journal of Symbolic Logic, vol. 5, no. 2, pp. 56--68, 1940.
[20]
M. Fiore, "An algebraic combinatorial approach to opetopic structure," talk at the Seminar on Higher Structures, Program on Higher Structures in Geometry and Physics, Max Planck Institute for Mathematics, Bonn (Germany), 2016. [Online]. Available: https://www.mpim-bonn.mpg.de/node/6586
[21]
N. Yamada and S. Abramsky, "Dynamic game semantics," arXiv, 2018. [Online]. Available: https://arxiv.org/abs/1601.04147
[22]
D. E. Rydeheard and J. G. Stell, "Foundations of equational deduction: A categorical treatment of equational proofs and unification algorithms," in Category Theory and Computer Science, D. H. Pitt, A. Poigné, and D. E. Rydeheard, Eds. Springer Berlin Heidelberg, 1987, pp. 114--139.
[23]
A. J. Power, "An abstract formulation for rewrite systems," in Category Theory and Computer Science, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts, and A. Poigné, Eds. Springer Berlin Heidelberg, 1989, pp. 300--312.
[24]
R. A. G. Seely, "Modelling computations: A 2-categorical framework," in Proceedings of the Second Annual IEEE Symp. on Logic in Computer Science, D. Gries, Ed. IEEE Computer Society Press, June 1987, pp. 65--71.
[25]
B. P. Hilken, "Towards a proof theory of rewriting: the simply typed 2λ-calculus," Theoretical Computer Science, vol. 170, no. 1, pp. 407--444, 1996.
[26]
C. B. Jay and N. Ghani, "The virtues of eta-expansion," Journal of Functional Programming, vol. 5, no. 2, pp. 135--154, 1995.
[27]
N. Ghani, "Adjoint rewriting," Ph.D. dissertation, University of Edinburgh, 1995.
[28]
N. Tabareau, "Aspect oriented programming: A language for 2-categories," in Proceedings of the 10th International Workshop on Foundations of Aspect-oriented Languages, ser. FOAL '11. ACM, 2011, pp. 13--17.
[29]
T. Hirschowitz, "Cartesian closed 2-categories and permutation equivalence in higher-order rewriting," Logical Methods in Computer Science, vol. 9, pp. 1--22, 07 2013.
[30]
P. Martin-Löf, Intuitionistic Type Theory. Bibliopolis, 1984.
[31]
D. R. Licata and R. Harper, "2-dimensional directed type theory," Electronic Notes in Theoretical Computer Science, vol. 276, pp. 263--289, 2011, twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII).
[32]
P.-L. Curien, "Substitution up to isomorphism," Fundam. Inf., vol. 19, no. 1-2, pp. 51--85, Sep. 1993.
[33]
The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: https://homotopytypetheory.org/book, 2013.
[34]
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Levy, "Explicit substitutions," in Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL '90. ACM, 1990, pp. 31--46.
[35]
E. Ritter and V. de Paiva, "On explicit substitutions and names (extended abstract)," in Automata, Languages and Programming, P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, Eds. Springer Berlin Heidelberg, 1997, pp. 248--258.
[36]
B. Plotkin, Universal Algebra, Algebraic Logic, and Databases. Springer, 1994.
[37]
R. Gordon, A. Power, and R. Street, Coherence for tricategories. Memoirs of the American Mathematical Society, 1995.
[38]
N. Gurski, Coherence in Three-Dimensional Category Theory. Cambridge University Press, 2013.
[39]
Agda contributors, "The Agda proof assistant," https://wiki.portal.chalmers.se/agda/pmwiki.php.
[40]
A. J. Power, "2-categories," BRICS Notes Series, 1998.
[41]
S. Mac Lane, Categories for the Working Mathematician, 2nd ed., ser. Graduate Texts in Mathematics. Springer-Verlag New York, 1998, vol. 5.
[42]
T. Fiore, Pseudo Limits, Biadjoints, and Pseudo Algebras: Categorical Foundations of Conformal Field Theory, ser. Memoirs of the American Mathematical Society. AMS, 2006.
[43]
F. W. Lawvere, "Adjoints in and among bicategories," in Logic & Algebra, ser. Lecture Notes in Pure and Applied Algebra, vol. 180, 1996, pp. 181--189.
[44]
S. Lack and R. Street, "Skew monoidales, skew warpings and quantum categories," Theory and Applications of Categories, 2012.
[45]
R. Street, "Fibrations in bicategories," Cahiers de Topologie et Géométrie Différentielle Catégoriques, vol. 21, no. 2, pp. 111--160, 1980.
[46]
S. Staton, "An algebraic presentation of predicate logic," in Foundations of Software Science and Computation Structures, F. Pfenning, Ed. Springer Berlin Heidelberg, 2013, pp. 401--417.
[47]
M. Fiore, "On the concrete representation of discrete enriched abstract clones," Tbilisi Mathematical Journal, vol. 10, no. 3, pp. 297--328, 2017.
[48]
K. Szlachányi, "Skew-monoidal categories and bialgebroids," Advances in Mathematics, vol. 231, no. 3, pp. 1694--1730, 2012.
[49]
T. Leinster, Higher operads, higher categories, ser. London Mathematical Society Lecture Note Series. Cambridge University Press, 2004, no. 298.
[50]
C. Hermida, "Representable multicategories," Advances in Mathematics, vol. 151, no. 2, pp. 164--225, 2000.
[51]
R. L. Crole, Categories for Types. Cambridge University Press, 1994.
[52]
A. Carboni and R. Walters, "Cartesian bicategories I," Journal of Pure and Applied Algebra, vol. 49, no. 1, pp. 11--32, 1987.
[53]
A. Carboni, G. Kelly, R. Walters, and R. Wood, "Cartesian bicategories II," Theory and Applications of Categories, vol. 19, no. 6, pp. 93--124, 2008.
Index Terms
- A type theory for cartesian closed bicategories
Index terms have been assigned to the content through auto-classification.
Recommendations
Observationally-induced Effects in Cartesian Closed Categories
Alex Simpson has suggested an observationally-induced approach towards obtaining monads for computational effects in denotational semantics. The underlying idea of this approach is to use a single observation algebra as computational prototype and to ...
Introduction to linear bicategories
Linear bicategories are a generalization of bicategories in which the one horizontal composition is replaced by two (linked) horizontal compositions. These compositions provide a semantic model for the tensor and par of linear logic: in particular, as ...
The largest Cartesian closed category of domains, considered constructively
This paper addresses a conjecture of Smyth that says that if $D$ and $[D \rightarrow D]$ are effectively algebraic directed-complete partial orders with least element (cpo's), then $D$ is an effectively strongly algebraic cpo, though what is meant by an ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
In-Cooperation
- EACSL: European Association for Computer Science Logic
- IEEE-CS\DATC: IEEE Computer Society
Publisher
IEEE Press
Publication History
Published: 08 June 2021
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
LICS '19
Sponsor:
LICS '19: 34th Annual ACM/IEEE Symposium on Logic in Computer Science
June 24 - 27, 2019
Vancouver, Canada
Acceptance Rates
Overall Acceptance Rate 215 of 622 submissions, 35%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 14Total Downloads
- Downloads (Last 12 months)4
- Downloads (Last 6 weeks)1
Reflects downloads up to 13 Nov 2024
Other Metrics
Citations
Cited By
View all- Olimpieri FGorla D(2021)Intersection type distributorsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470617(1-15)Online publication date: 29-Jun-2021
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in