Dialectica Categories

A place to collect work on dialectica categories.

My work:

1. Thesis: "The Dialectica Categories", TR213 from Cambridge, https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-213.pdf, 1990 videos Dialectica for Friends https://www.youtube.com/watch?v=hJrJSZlO-Ic and Dialectica: the mathematical version https://www.youtube.com/watch?v=GRdrN6L3UCc&t=3s

From thesis, two conference papers and a much later journal comparison:

2. AMS vol 92: "The Dialectica Categories" Boulder volume, http://www.cs.bham.ac.uk/~vdp/publications/dial87.pdf, 1989

3. CTCS 1989: "A Dialectica-like Model of Linear Logic", http://www.cs.bham.ac.uk/~vdp/publications/CTCS89.pdf, 1989

4. TAC paper "Dialectica and Chu constructions: cousins?", Theory and Applications of Categories, Vol. 17, No. 7, pp 127-152, 2006. http://www.tac.mta.ca/tac/volumes/17/7/17-07abs.html

From thesis a new logical/type theory system that is the natural, intrinsic logic of the categories GC, "Full Intuitionistic Linear Logic" (FILL), and with Luiz Carlos a version for Intuitionistic logic (FIL). With Torben and Harley proofs of cut-elimination for the logic FILL.

5. Full Intuitionistic Linear Logic (with Martin Hyland) APAL, 1993. https://www.sciencedirect.com/science/article/pii/0168007293901465 (official) https://www.cs.bham.ac.uk/~vdp/publications/fill.pdf (preprint)

6. Full Intuitionistic Logic (with Luiz Carlos Pereira) Logic Colloquium 1994 -- abstract only. paper in 2005, "A short note on Intuitionistic Propositional Logic with Multiple Conclusions" Manuscrito-- Rev Int. Fil. Campinas, v. 28, n.2, pp 317-329, jul-dez, 2005 (https://www.cs.bham.ac.uk/%7Evdp/publications/fil.pdf) --this is intuitionistic logic, not Linear Logic!

7. Cut-Elimination for Full Intuitionistic Linear Logic (with Torben Brauner), CSL1997, preprint https://www.brics.dk/RS/96/10/index.html CSL version `A formulation of linear logic based on dependency-relations'- T Braüner, V De Paiva Int Workshop on Computer Science Logic, 129-148, 1997 (https://www.researchgate.net/publication/221557909_A_Formulation_of_Linear_Logic_Based_on_Dependency-Relations)

8. FILL (new proof of cut-elimination with Harley Eades III) Multiple Conclusion Linear Logic: Cut-elimination and more. https://academic.oup.com/logcom/article-abstract/30/1/157/5745861?redirectedFrom=fulltext Lecture Notes in Computer Science, 04 January 2016. Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS 2016), formalized in Agda. Journal version submitted.

Appeared in Journal of Logic and Computation, Feb 2020 https://academic.oup.com/logcom/article-abstract/30/1/157/5745861?redirectedFrom=fulltext

9. Typed lambda-calculus for FILL (with Eike Ritter) "A Parigot-style linear λ-calculus for Full intuitionistic Linear Logic", 2007 https://www.cs.bham.ac.uk/%7Evdp/publications/fillmu.pdf

Algebraic versions:

10. Lineales, in "O que nos faz pensar?" 1991 https://www.cs.bham.ac.uk/~vdp/publications/Lineales91.pdf

    Lineales: algebras and categories in the semantics of Linear Logic. Presented at LLC8, Stanford, May 1999. Revised version appears in CSLI book "Words, Proofs, and Diagrams" (eds. D. Barker-Plummer, D. Beaver, Johan van Benthem, and P. Scotto di Luzio), 2002 Official version: (https://drive.google.com/file/d/1Xk-2LKABGNfnYTf9CGV6lkhWBUHpGT9m/view?usp=sharing). Original version Lineales: Algebraic Models of Linear Logic from a Categorical Perspective, https://drive.google.com/file/d/11BMFAOhACYHa7asGf5i2DuRywWQjSmp1/view?usp=sharing.

Applications:

11. BRICS TR: "A linear specification language for Petri Nets", http://www.cs.bham.ac.uk/~vdp/publications/LinSpecPetri.pdf accepted for TCS in mid 90's, but then abandoned. short note for LSFA2018 based on this work, rejected.

Carolyn Brown thesis now at https://era.ed.ac.uk/bitstream/handle/1842/15424/Brown1990.Pdf?sequence=1

12. Theme of work in ACT Adjoint School 2020 with Elena Di Lavore, Xiaoyan Li, Wilmer Leal, Eigil Rischel and Jade Master. Blog post in https://golem.ph.utexas.edu/category/2020/07/linear_logic_flavoured_composi.html. Also in https://www.appliedcategorytheory.org/adjoint-school-act-2020/dialectica-categories-of-petri-nets/

Poster at ACT 2021, presented by Elena, ACT-PN-poster, https://drive.google.com/file/d/1rM6MCHl0FHfOOCIHA4irVwl-tuadYha-/view?usp=sharing

Preprint 2021: Dialectica Petri Nets https://arxiv.org/abs/2105.12801, submitted

13. "Categorical multirelations, linear logic and Petri nets" TR from Cambridge http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-225.pdf

13a. LL applied to intuitionistic logic FIL (Full Intuitionistic Logic) with Luiz Carlos Pereira,

1. abstract "A New Proof System for Intuitionistic Logic" (with L. C. Pereira) The Bulletin of Symbolic Logic, vol 1(1):101, 1995

2. paper "A short note on Intuitionistic Propositional Logic with Multiple Conclusions" (with Luiz Carlos Pereira) Manuscrito-- Rev Int. Fil. Campinas, v. 28, n.2, pp 317-329, jul-dez, 2005. https://www.researchgate.net/publication/228619994_A_short_note_on_intuitionistic_propositional_logic_with_multiple_conclusions

Dialectica categories for Lambek calculus.

14. Paper in Amsterdam Colloquium 1991 https://www.researchgate.net/publication/2288039_A_Dialectica_Model_of_the_Lambek_Calculus

15. Talk at APA, April 2017 conference LFCS paper with Harley Eades III, appeared in Jan2018, https://arxiv.org/abs/1801.06883 journal paper not submitted, yet (?)

16. Dialectica categories for modelling State/Pomset logic: A Dialectica Model of State (1996) Conference paper in CATS'1996 with Correa and Hauesler. https://www.academia.edu/674289/A_dialectica_model_of_state

17. journal paper: Valeria de Paiva. Linear Logic Model of State Revisited. Logic Journal of IGPL, 01 October 2014. volume 22, number 5, pages 791-804. http://vcvpaiva.github.io/includes/pubs/2014-LL-model.pdf

18. Dialectica categories for Relevant logic (need to recover the important bits from http://www.dbd.puc-rio.br/depto_informatica/93_mere.pdf) slides?

Dialectica categories for Set Theory, work with Samuel G da Silva. Three papers so far, 19, 20 and 21.

19. Dialectica Categories, Cardinalities of the Continuum and Combinatorics of Ideals, with Samuel G. da Silva. Available from https://www.researchgate.net/publication/315001808_Dialectica_Categories_Cardinalities_of_the_Continuum_and_Combinatorics_of_Ideals

20. Linear Natural Numbers Objects in Dial (Valeria de Paiva, Charles Morgan, Samuel G. da Silva). Natural Number Objects in Dialectica Categories. ENTCS, 01 January 2014. Electronic Notes in theoretical Computer Science, 305 (2014), pages 53-65. https://www.researchgate.net/publication/263699584_Natural_Number_Objects_in_Dialectica_Categories)

21. Kolgomorov-Veloso Problems and Dialectica Categories, (with Samuel G. da Silva). In "A Question is More Illuminating than the Answer: A Festschrift for Paulo A.S. Veloso Edward Hermann Haeusler, Luiz Carlos Pinheiro Dias Pereira and Jorge Petrucio Viana, eds.

Preprint arXiv https://arxiv.org/abs/2107.07854

Samuel, on his own, based on Dialectica:

• "Reductions between certain incidence problems and the continuum hypothesis" -- http://www.ejournals.eu/rml/2019/Number-54/art/14434/

• "The Axiom of Choice and the Partition Principle from Dialectica Categories" -- slides from the meeting "Cantor Meets Robinson" https://cantormeetsrobinson.files.wordpress.com/2019/04/gdasilva.pdf Samuel G Da Silva, The Axiom of Choice and the Partition Principle from Dialectica Categories, Logic Journal of the IGPL, 2020;, jzaa023, https://doi.org/10.1093/jigpal/jzaa023

22. Dialectica over a partial order, in LC Pereira Festschrift, http://vcvpaiva.github.io/includes/pubs/2015boundedDial.pdf

23. Generalizations:

Dialectica Principles via Gödel Doctrines (with Davide Trotta and Matteo Spadetto) Theoretical Computer Science, 2023. https://trottadavide.github.io/publication/pubb_6/ Preprint in the arXiv https://arxiv.org/abs/2104.14021

Dialectica logical principles: not only rules. (with Davide Trotta and Matteo Spadetto) Journal of Logic and Computation, 2022. https://trottadavide.github.io/publication/pubb_4/

Dialectica Logical Principles (with Davide Trotta and Matteo Spadetto) in LFCS2022. https://trottadavide.github.io/publication/pubb_3/ Preprint in the arXiv https://arxiv.org/abs/2109.08064

The Gödel fibration. (with Davide Trotta and Matteo Spadetto) In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), 2021. see https://trottadavide.github.io/publication/pubb_2/

24. Dialectica and Games (lost EPSRC proposal, how did I do that?)

24A. SuperPower Lorenzen Games, manuscript from 2011 Nancy CLMPST Talk. https://drive.google.com/file/d/19wSFHBNdb-PQj2ZjM6oZtV6MVutpGIdn/view?usp=sharing

Extreme cases of Dialectica with Andrea Schalk

25. Building models of linear logic, V De Paiva, A Schalk (https://www.researchgate.net/publication/220977218_Building_Models_of_Linear_Logic) International Conference on Algebraic Methodology and Software Technology

26. Poset-valued sets or how to build models for linear logics A Schalk, V De Paiva Theoretical Computer Science 315 (1), 83-107 https://www.researchgate.net/publication/222848911_Poset-valued_sets_or_how_to_build_models_for_linear_logics

==================================================

Work (from others) related to dialectica categories:

0. M. Hyland, Proof Theory in the Abstract 2002 https://www.sciencedirect.com/science/article/pii/S0168007201000756

1. Hofstra, P in Makkai Festschrifft, 2011 The dialectica monad and its cousins, Pieter J. W. Hofstra, http://mysite.science.uottawa.ca/phofstra/dialectica.pdf

2. Bodil Biering's thesis, Dialectica Interpretations: A Categorical Analysis http://cs.au.dk/~birke/phd-students/BieringB-thesis.pdf, 2008

3. An Analysis of Gödel's dialectica Interpretation via Linear Logic, Paulo Oliva, Dialectica, 2008. (available from http://www.eecs.qmul.ac.uk/~pbo/) many more from his webpage!

4. "A Functional Functional Interpretation", Pierre-Marie Pedrot, LICS 2014, https://www.pédrot.fr/articles/lics2014.pdf https://www.pédrot.fr/slides/thesis-09-15.pdf, the thesis https://hal.archives-ouvertes.fr/tel-01247085

also slides post-thesis https://www.xn--pdrot-bsa.fr/slides/types-dialectica-05-16.pdf

5. Mihai Budiu, Joel Galenson, and Gordon Plotkin The Compiler Forest, ESOP 2013, http://budiu.info/work/esop13.pdf slides https://jgalenson.github.io/papers/esop2013-talk.pdf

6. Jules Hedge's Dialectica categories and games with bidding. In Post-proceedings of TYPES’14. LIPIcs 39:89-110, 2015. http://drops.dagstuhl.de/opus/volltexte/2015/5493/pdf/7.pdf

Also influential blog post Lenses for Philosophers https://julesh.com/2018/08/16/lenses-for-philosophers/

a. Tamara von Glehn. Polynomials and models of type theory (PhD thesis) https://www.repository.cam.ac.uk/handle/1810/254394, 2015

b. Sean Moss and Tamara von Glehn. Dialectica models of type theory, LiCS2018. https://dl.acm.org/citation.cfm?doid=3209108.3209207 paywall, now https://arxiv.org/abs/2105.00283?context=math

c. Sean Moss. PhD thesis: The Dialectica models of type theory (Diller-Nahm) https://www.repository.cam.ac.uk/handle/1810/280672

d. Tamara von Glehn POLYNOMIALS, FIBRATIONS AND DISTRIBUTIVE LAWS, http://www.tac.mta.ca/tac/volumes/33/36/33-36.pdf

e. Sean Moss. Talk at Polynomial Workshop 2: Dependent products of polynomials https://topos.site/p-func-workshop/slides/Moss.pdf

8. Tom Powell a. Applying Gödel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma, https://arxiv.org/abs/1210.3117.

   b. Well Quasi-Orders and the Functional Interpretation, https://arxiv.org/pdf/1706.02881.pdf

   c. LICS2017 paper "Gödel's functional interpretation and the concept of learning" http://dl.acm.org/citation.cfm?doid=2933575.2933605

9. Mike Shulman a. The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions, https://arxiv.org/abs/1806.06082

   b. Mike Shulman, Linear logic for constructive mathematics, https://arxiv.org/abs/1805.07518 (check also https://arxiv.org/abs/1107.6032 Traces in symmetric monoidal categories and https://golem.ph.utexas.edu/category/2017/12/the_2dialectica_construction_a.html)

10. Pierre Pradic and Colin Riba, from http://perso.ens-lyon.fr/colin.riba/ a. A Dialectica-Like Interpretation of a Linear MSO on Infinite Words. Submitted [pdf].

    b. LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic. LICS'18 [pdf].

    c. A Curry-Howard Approach to Church's Synthesis. FSCD'17 [pdf]. Long version (submitted) [pdf].

11. Pierre Hyvernat, A Linear Category of Polynomial Diagrams, http://www.lama.univ-savoie.fr/pagesmembres/hyvernat/research.php

    https://www.lama.univ-savoie.fr/pagesmembres/hyvernat/Files/poly_functors.pdf

    https://www.lama.univ-savoie.fr/pagesmembres/hyvernat/Files/poly_diagrams.pdf

12. Benno van der Berg et al A functional interpretation for nonstandard arithmetic with Eyvind Briseid and Pavol Safarik. Annals of Pure and Applied Logic, volume 163, issue 12 (2012), pp. 1962–1994.

    https://staff.fnwi.uva.nl/b.vandenberg3/papers/dsttopos.pdf.

13. Martin Hyland's talk in Leeds "Polynomials and Dialectica categories" https://eps.leeds.ac.uk/maths/events/event/5993/polynomials-and-dialectica-categories

14. "The Dialectica Interpretation of first-order Classical Affine Logic", M. Shirahata, http://emis.impa.br/EMIS/journals/TAC/volumes/17/4/17-04.pdf

15. "A Semantic Version of the Diller-Nahm Variant of Godel’s Dialectica Interpretation" Thomas Streicher -- https://www2.mathematik.tu-darmstadt.de/~streicher/Dial.pdf

16. Pino Rosolini -- "Triposes and Gödel's Dialectica Interpretation" https://www.youtube.com/watch?v=_db-eVaU-ts

17. Hongde Hu; Andre Joyal -- Coherence completions of categories, https://core.ac.uk/download/pdf/82827543.pdf

18. Kerjean and Pedrot: ∂ is for Dialectica: typing differentiable programming, https://www.irif.fr/~kerjean/papers/dial_diff.pdf

Make a list of the work on Lenses! and containers -- see https://www.brunogavranovic.com/posts/2022-02-10-optics-vs-lenses-operationally.html and applications in his github Make a list of work on games