{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T08:08:28Z","timestamp":1648800508322},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2017,3,20]],"date-time":"2017-03-20T00:00:00Z","timestamp":1489968000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2018,6]]},"abstract":"<jats:p>Any refinement system (= functor) has a fully faithful representation in the refinement system of presheaves, by interpreting types as relative slice categories, and refinement types as presheaves over those categories. Motivated by an analogy between side effects in programming and<jats:italic>context effects<\/jats:italic>in linear logic, we study logical aspects of this \u2018positive\u2019 (covariant) representation, as well as of an associated \u2018negative\u2019 (contravariant) representation. We establish several preservation properties for these representations, including a generalization of Day's embedding theorem for monoidal closed categories. Then, we establish that the positive and negative representations satisfy an Isbell-style duality. As corollaries, we derive two different formulas for the positive representation of a pushforward (inspired by the classical negative translations of proof theory), which express it either as the dual of a pullback of a dual or as the double dual of a pushforward. Besides explaining how these constructions on refinement systems generalize familiar category-theoretic ones (by viewing categories as special refinement systems), our main running examples involve representations of Hoare logic and linear sequent calculus.<\/jats:p>","DOI":"10.1017\/s0960129517000068","type":"journal-article","created":{"date-parts":[[2017,3,20]],"date-time":"2017-03-20T14:03:08Z","timestamp":1490018588000},"page":"736-774","source":"Crossref","is-referenced-by-count":0,"title":["An Isbell duality theorem for type refinement systems"],"prefix":"10.1017","volume":"28","author":[{"given":"PAUL-ANDR\u00c9","family":"MELLI\u00c8S","sequence":"first","affiliation":[]},{"given":"NOAM","family":"ZEILBERGER","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2017,3,20]]},"reference":[{"key":"S0960129517000068_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002508"},{"key":"S0960129517000068_ref32","first-page":"303","article-title":"Church and curry: Combining intrinsic and extrinsic typing","volume":"17","author":"Pfenning","year":"2008","journal-title":"Studies in Logic"},{"key":"S0960129517000068_ref28","unstructured":"Melli\u00e8s P.-A. and Zeilberger N. (2013). Type refinement and monoidal closed bifibrations. Unpublished manuscript. arXiv:1310.0263."},{"key":"S0960129517000068_ref20","volume-title":"Deductive Systems and Categories II","author":"Lambek","year":"1969"},{"key":"S0960129517000068_ref4","volume-title":"Handbook of Categorical Algebra 2: Categories and Structures","author":"Borceux","year":"1994"},{"key":"S0960129517000068_ref17","volume-title":"Categorical Logic and Type Theory","author":"Jacobs","year":"1999"},{"key":"S0960129517000068_ref13","doi-asserted-by":"crossref","unstructured":"Hermida C. (November 1993). Fibrations, Logical predicates and indeterminates, Ph.D. thesis, University of Edinburgh.","DOI":"10.7146\/dpb.v22i462.6935"},{"key":"S0960129517000068_ref26","unstructured":"Maltsiniotis G. (2005). La th\u00e9orie de l'homotopie de Grothendieck, Ast\u00e9risque."},{"key":"S0960129517000068_ref1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"S0960129517000068_ref29","unstructured":"Melli\u00e8s P.-A. and Zeilberger N. (2015). Functors are type refinement systems. In: Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming 3\u201316."},{"key":"S0960129517000068_ref23","first-page":"1","article-title":"Taking categories seriously","volume":"8","author":"Lawvere","year":"2005","journal-title":"Reprints in Theory and Applications of Categories"},{"key":"S0960129517000068_ref11","volume-title":"Reflections on the Work of C.A.R. Hoare","author":"Gordon","year":"2010"},{"key":"S0960129517000068_ref19","volume-title":"Basic Concepts in Enriched Category Theory","author":"Kelly","year":"1982"},{"key":"S0960129517000068_ref30","unstructured":"Melli\u00e8s P.-A. and Zeilberger N. (2016). A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science 555\u2013564."},{"key":"S0960129517000068_ref2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:9)2012"},{"key":"S0960129517000068_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129517000068_ref7","unstructured":"Fiore M. (2002). Semantic analysis of normalisation by evaluation for typed Lambda calculus (Extended Abstract). In: Proceedings of the 4th International Conference on Principles and Practice of Declarative Programming 26\u201337."},{"key":"S0960129517000068_ref16","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1966-11541-0"},{"key":"S0960129517000068_ref8","volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen","year":"1969"},{"key":"S0960129517000068_ref12","unstructured":"Hasegawa M. (1999). Categorical glueing and logical predicates for models of linear logic. Technical Report RIMS-1223, Research Institute for Mathematical Sciences, Kyoto University."},{"key":"S0960129517000068_ref3","unstructured":"B\u00e9nabou J. (2000). Distributors at work. Notes from a course at TU Darmstadt in June 2000, taken by Thomas Streicher."},{"key":"S0960129517000068_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525896"},{"key":"S0960129517000068_ref27","unstructured":"Melli\u00e8s P.-A. (2012). Game semantics in string diagrams. In: Proceedings of the 27th Annual IEEE Conference on Logic in Computer Science 481\u2013490."},{"key":"S0960129517000068_ref21","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"S0960129517000068_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060438"},{"key":"S0960129517000068_ref14","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"S0960129517000068_ref33","unstructured":"Thielecke H. (1997). Categorical structure of continuation passing style, Ph.D. thesis, University of Edinburgh."},{"key":"S0960129517000068_ref31","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"S0960129517000068_ref9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-9(3:6)2013","article-title":"Indexed induction and coinduction, fibrationally","volume":"9","author":"Ghani","year":"2013","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129517000068_ref15","doi-asserted-by":"crossref","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Communications of the ACM"},{"key":"S0960129517000068_ref18","unstructured":"Katsumata S.-Y. (2002). A semantic formulation of \u22a4\u22a4-lifting and logical predicates for computational metalanguage. CSL 2005."},{"key":"S0960129517000068_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S0960129517000068_ref22","doi-asserted-by":"crossref","unstructured":"Lawvere F.W. (1970). Equality in hyperdoctrines and comprehension schema as an adjoint functor. In: Proceedings of the AMS Symposium on Pure Mathematics XVII 1\u201314.","DOI":"10.1090\/pspum\/017\/0257175"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129517000068","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T00:15:56Z","timestamp":1568938556000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129517000068\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,20]]},"references-count":33,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["S0960129517000068"],"URL":"https:\/\/doi.org\/10.1017\/s0960129517000068","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,20]]}}}