@incollection(a78,
 author       = {Peter Aczel},
 year         = {1978},
 title        = {The type theoretic interpretation of constructive set theory},
 booktitle    = {Logic {C}olloquium '77 ({P}roc. {C}onf., {W}roc\l aw, 1977)},
 series       = {Stud. Logic Foundations Math.},
 volume       = {96},
 publisher    = {North-Holland},
 address      = {Amsterdam},
 pages        = {55--66},
 doi          = {10.1016/S0049-237X(08)71989-X},
)
@incollection(a82,
 author       = {Peter Aczel},
 year         = {1982},
 title        = {The type theoretic interpretation of constructive set theory: choice principles},
 booktitle    = {The {L}. {E}. {J}. {B}rouwer {C}entenary {S}ymposium ({N}oordwijkerhout, 1981)},
 series       = {Stud. Logic Found. Math.},
 volume       = {110},
 publisher    = {North-Holland},
 address      = {Amsterdam},
 pages        = {1--40},
 doi          = {10.1016/S0049-237X(09)70120-X},
)
@incollection(a86,
 author       = {Peter Aczel},
 year         = {1986},
 title        = {The type theoretic interpretation of constructive set theory: inductive definitions},
 booktitle    = {Logic, methodology and philosophy of science, {VII} ({S}alzburg, 1983)},
 series       = {Stud. Logic Found. Math.},
 volume       = {114},
 publisher    = {North-Holland},
 address      = {Amsterdam},
 pages        = {17--49},
 doi          = {10.1016/S0049-237X(09)70683-4},
)
@article(aczel:aspects,
 author       = {Peter Aczel},
 year         = {2006},
 title        = {Aspects of general topology in constructive set theory},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {137},
 number       = {1--3},
 pages        = {3--29},
 doi          = {10.1016/j.apal.2005.05.016},
)
@techreport(aczel:notes,
 author       = {Peter Aczel and Michael Rathjen},
 year         = {2000},
 title        = {Notes on Constructive Set Theory},
 type         = {Technical Report},
 institution  = {Institut Mittag--Leffler},
 note         = {Report No. 40},
)
@unpublished(aczel:cstdraft,
 author       = {Peter Aczel and Michael Rathjen},
 year         = {2010},
 title        = {{Constructive set theory}},
 url          = {https://www1.maths.leeds.ac.uk/~rathjen/book.pdf},
 note         = {Book draft},
)
@article(Bellin2014,
 author       = {Gianluigi Bellin},
 year         = {2014},
 title        = {Categorical Proof Theory of Co-Intuitionistic Linear Logic},
 journal      = {Logical Methods in Computer Science},
 volume       = {10},
 number       = {3},
 doi          = {10.2168/lmcs-10(3:16)2014},
)
@article(van:kuroda,
 author       = {Benno van den Berg},
 year         = {2018},
 title        = {A {K}uroda-style $j$-translation},
 journal      = {Arch. Math. Log.},
 doi          = {10.1007/s00153-018-0656-x},
)
@incollection(bez:ax,
 author       = {Jean-Yves B\'eziau},
 year         = {2006},
 title        = {Les axiomes de {T}arski},
 editor       = {Roger Pouivet and Manuel Resbuschi},
 booktitle    = {La philosophie en {P}ologne 1919-1939},
 publisher    = {Librairie Philosophique J. VRIN},
 address      = {Paris},
)
@misc(blkov2019proof,
 author       = {Marta B{\'i}lkov{\'a} and Almudena Colacito},
 year         = {2019},
 title        = {Proof Theory for Positive Logic with Weak Negation},
 eprint       = {1907.05411},
)
@book(Bishop67,
 author       = {Errett Bishop},
 year         = {1967},
 title        = {Foundations of Constructive Analysis},
 publisher    = {McGraw-Hill},
 address      = {New York},
)
@book(Bishop-Bridges85,
 author       = {Errett Bishop and Douglas Bridges},
 year         = {1985},
 title        = {Constructive Analysis},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-61667-9},
)
@incollection(cedcoq:entaildistr,
 author       = {Jan {Cederquist} and Thierry {Coquand}},
 year         = {2000},
 title        = {{Entailment relations and distributive lattices}},
 editor       = {Samuel R. Buss and Petr H{\'a}jek and Pavel Pudl{\'a}k},
 booktitle    = {{Logic {C}olloquium '98. Proceedings of the {A}nnual {E}uropean {S}ummer {M}eeting of the {A}ssociation for {S}ymbolic Logic, {P}rague, {C}zech {R}epublic, {A}ugust 9--15, 1998}},
 series       = {Lect.~Notes Logic},
 volume       = {13},
 publisher    = {A.~K.~Peters},
 address      = {Natick, MA},
 pages        = {127--139},
 doi          = {10.1017/9781316756140.011},
)
@article(cintula:pbc,
 author       = {Petr Cintula and Noguera Carles},
 year         = {2013},
 title        = {The Proof by Cases Property and its Variants in Structural Consequence Relations},
 journal      = {Studia Logica},
 volume       = {101},
 number       = {4},
 pages        = {713--747},
 doi          = {10.1007/s11225-013-9496-1},
)
@article(cir:conv,
 author       = {Francesco Ciraulo and Maria Emilia Maietti and Giovanni Sambin},
 year         = {2013},
 title        = {Convergence in formal topology: a unifying notion},
 journal      = {J.~Log.~Anal.},
 volume       = {5},
 number       = {2},
 pages        = {1--45},
 doi          = {10.4115/jla.2013.5.2},
)
@article(Ciraulo:finitary,
 author       = {Francesco Ciraulo and Giovanni Sambin},
 year         = {2008},
 title        = {{Finitary formal topologies and Stone's representation theorem}},
 journal      = {Theoret.~Comput.~Sci.},
 volume       = {405},
 number       = {1--2},
 pages        = {11--23},
 doi          = {10.1016/j.tcs.2008.06.020},
)
@misc(coquand:dlhb,
 author       = {Thierry Coquand},
 year         = {2000},
 title        = {A direct proof of the localic {H}ahn-{B}anach theorem},
 url          = {http://www.cse.chalmers.se/~coquand/formal.html},
)
@misc(coquand:lc,
 author       = {Thierry Coquand},
 year         = {2000},
 title        = {{Lewis Carroll, Gentzen and entailment relations}},
 url          = {http://www.cse.chalmers.se/~coquand/formal.html},
)
@article(coq:stone,
 author       = {Thierry Coquand},
 year         = {2005},
 title        = {About {S}tone's notion of spectrum},
 journal      = {J.~Pure Appl.~Algebra},
 volume       = {197},
 number       = {1--3},
 pages        = {141--158},
 doi          = {10.1016/j.jpaa.2004.08.024},
)
@article(coq:valspace,
 author       = {Thierry Coquand},
 year         = {2009},
 title        = {Space of valuations},
 journal      = {Ann.~Pure Appl.~Logic},
 volume       = {157},
 pages        = {97--109},
 doi          = {10.1016/j.apal.2008.09.003},
)
@inproceedings(coq:hidden-krull,
 author       = {Thierry Coquand and Henri Lombardi},
 year         = {2002},
 title        = {Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings},
 editor       = {M. Fontana and S.-E. Kabbaj and S. Wiegand},
 booktitle    = {Commutative {R}ing {T}heory and {A}pplications},
 series       = {Lect.~{N}otes {P}ure {A}ppl.~{M}athematics},
 volume       = {231},
 publisher    = {Addison-Wesley},
 address      = {Reading, MA},
 pages        = {477--499},
)
@article(cln:groups,
 author       = {Thierry Coquand and Henri Lombardi and Stefan Neuwirth},
 year         = {2019},
 title        = {Lattice-ordered groups generated by an ordered group and regular systems of ideals},
 journal      = {Rocky Mountain J.~Math.},
 volume       = {49},
 number       = {5},
 pages        = {1449--1489},
 doi          = {10.1216/RMJ-2019-49-5-1449},
)
@unpublished(coq:lorenzen,
 author       = {Thierry Coquand and Stefan Neuwirth},
 year         = {2017},
 title        = {{An introduction to Lorenzen's {``Algebraic and logistic investigations on free lattices''} (1951)}},
 url          = {https://arxiv.org/abs/1711.06139},
 note         = {Preprint},
)
@article(coq:prague,
 author       = {Thierry Coquand and Henrik Persson},
 year         = {2001},
 title        = {Valuations and {D}edekind's {P}rague theorem},
 journal      = {J.~Pure Appl.~Algebra},
 volume       = {155},
 number       = {2--3},
 pages        = {121--129},
 doi          = {10.1016/S0022-4049(99)00095-X},
)
@incollection(coq:seq,
 author       = {Thierry Coquand and Guo-Qiang Zhang},
 year         = {2000},
 title        = {Sequents, frames, and completeness},
 editor       = {{Peter G.} Clote and Helmut Schwichtenberg},
 booktitle    = {Computer Science Logic ({F}ischbachau, 2000)},
 series       = {Lecture Notes in Comput.~Sci.},
 volume       = {1862},
 publisher    = {Springer, Berlin},
 pages        = {277--291},
 doi          = {10.1007/3-540-44622-2_18},
)
@book(dvd:las,
 author       = {Dirk van Dalen},
 year         = {2013},
 title        = {Logic and Structure},
 edition      = {fifth},
 series       = {Universitext},
 publisher    = {Springer},
 address      = {London},
 doi          = {10.1007/978-1-4471-4558-5},
)
@article(esca:peirce,
 author       = {Mart{\'i}n Escard{\'o} and Paulo Oliva},
 year         = {2012},
 title        = {The {P}eirce translation},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {163},
 pages        = {681--692},
 doi          = {10.1016/j.apal.2011.11.002},
)
@article(esp:gli,
 author       = {Esp\'{\i}ndola, Christian},
 year         = {2013},
 title        = {A short proof of {G}livenko theorems for intermediate predicate logics},
 journal      = {Arch. Math. Logic},
 volume       = {52},
 number       = {7-8},
 pages        = {823--826},
 doi          = {10.1007/s00153-013-0346-7},
)
@article(Fair97,
 author       = {Matt {Fairtlough} and Michael {Mendler}},
 year         = {1997},
 title        = {{Propositional lax logic}},
 journal      = {{Inf.~and Comput.}},
 volume       = {137},
 number       = {1},
 pages        = {1--33},
 doi          = {10.1006/inco.1997.2627},
)
@misc(fel:msc,
 author       = {Giulio Fellin},
 year         = {2018},
 title        = {{The Jacobson Radical: from Algebra to Logic}},
 howpublished = {Master's thesis. Universit\`a di Verona, Dipartimento di Informatica},
)
@incollection(fel:jac:proc,
 author       = {Giulio Fellin and Peter Schuster and Daniel Wessel},
 year         = {2019},
 title        = {The {J}acobson {R}adical of a {P}ropositional {T}heory},
 editor       = {Thomas Piecha and Schroeder-Heister, Peter},
 booktitle    = {Proof-Theoretic Semantics: Assessment and Future Perspectives. Proceedings of the Third T{\"u}bingen Conference on Proof-Theoretic Semantics, 27--30 March 2019},
 publisher    = {University of T{\"u}bingen},
 pages        = {287--299},
 doi          = {10.15496/publikation-35319},
)
@article(fel:jac,
 author       = {Giulio Fellin and Peter Schuster and Daniel Wessel},
 year         = {2019},
 title        = {The {J}acobson radical of a propositional theory},
 note         = {Submitted},
)
@incollection(fri:translation,
 author       = {Harvey Friedman},
 year         = {1978},
 title        = {Classical and intuitionistically provably recursive functions},
 editor       = {G.H. M\"uller and D.S. Scott},
 booktitle    = {Higher Set Theory},
 series       = {LNM},
 volume       = {669},
 publisher    = {Springer},
 address      = {New York},
 pages        = {21--27},
 doi          = {10.1007/BFb0103100},
)
@article(10.2307/27588518,
 author       = {Nikolaos Galatos and Hiroakira Ono},
 year         = {2006},
 title        = {Glivenko Theorems for Substructural Logics over {FL}},
 journal      = {The Journal of Symbolic Logic},
 volume       = {71},
 number       = {4},
 pages        = {1353--1384},
 doi          = {10.2178/jsl/1164060460},
)
@article(gliv29,
 author       = {Valery Glivenko},
 year         = {1929},
 title        = {Sur quelques points de la {L}ogique de {M}.~{B}rouwer},
 journal      = {Acad. Roy. Belg. Bull. Cl. Sci. (5)},
 volume       = {15},
 pages        = {183--188},
)
@article(gue:pos,
 author       = {Giulio Guerrieri and Alberto Naibo},
 year         = {2019},
 title        = {Postponement of {$\mathsf{raa}$} and {G}livenko's theorem, revisited},
 journal      = {Studia Logica},
 volume       = {107},
 number       = {1},
 pages        = {109--144},
 doi          = {10.2178/jsl/1231082306},
)
@article(hayk:more,
 author       = {Levon Haykazyan},
 year         = {2020},
 title        = {More on a curious nucleus},
 journal      = {J. Pure Appl. Algebra},
 volume       = {224},
 pages        = {860--868},
 doi          = {10.1016/j.jpaa.2019.06.014},
)
@article(hertz:1,
 author       = {Paul Hertz},
 year         = {1922},
 title        = {{\"Uber Axiomensysteme f\"ur beliebige Satzsysteme. I. Teil. S\"atze ersten Grades}},
 journal      = {Math.~Ann.},
 volume       = {87},
 number       = {3},
 pages        = {246--269},
 doi          = {10.1007/BF01459067},
)
@article(hertz:2,
 author       = {Paul Hertz},
 year         = {1923},
 title        = {{\"Uber Axiomensysteme f\"ur beliebige Satzsysteme. II. Teil. S\"atze h\"oheren Grades}},
 journal      = {Math.~Ann.},
 volume       = {89},
 number       = {1},
 pages        = {76--102},
 doi          = {10.1007/BF01448090},
)
@article(hertz:3,
 author       = {Paul Hertz},
 year         = {1929},
 title        = {{\"Uber Axiomensysteme f\"ur beliebige Satzsysteme}},
 journal      = {Math.~Ann.},
 volume       = {101},
 number       = {1},
 pages        = {457--514},
 doi          = {10.1007/BF01454856},
)
@article(DBLP:journals/mlq/IshiharaN16,
 author       = {Hajime Ishihara and Takako Nemoto},
 year         = {2016},
 title        = {A note on the independence of premiss rule},
 journal      = {Math. Log. Q.},
 volume       = {62},
 number       = {1-2},
 pages        = {72--76},
 doi          = {10.1002/malq.201500032},
)
@article(ish:emb,
 author       = {Hajime Ishihara and Helmut Schwichtenberg},
 year         = {2016},
 title        = {Embedding classical in minimal implicational logic},
 journal      = {MLQ Math.~Log.~Q.},
 volume       = {62},
 number       = {1-2},
 pages        = {94--101},
 doi          = {10.1002/malq.201400099},
)
@book(joh:sto,
 author       = {Peter T. Johnstone},
 year         = {1982},
 title        = {Stone {S}paces.},
 series       = {Cambridge Studies in Advanced Mathematics},
 volume       = {3},
 publisher    = {Cambridge University Press},
)
@article(Kracht1998,
 author       = {Marcus Kracht},
 year         = {1998},
 title        = {On Extensions of Intermediate Logics by Strong Negation},
 journal      = {Journal of Philosophical Logic},
 volume       = {27},
 number       = {1},
 doi          = {10.1023/A:1004222213212},
)
@incollection(leg:her,
 author       = {Javier Legris},
 title        = {Paul {H}ertz and the origins of structural reasoning},
 editor       = {Jean-Yves B{\'e}ziau},
 booktitle    = {Universal Logic: An Anthology. From Paul Hertz to Dov Gabbay},
 series       = {Studies in Universal Logic},
 publisher    = {Birkh{\"a}user},
 address      = {Basel},
 pages        = {3--10},
 doi          = {10.1007/978-3-0346-0145-0_1},
)
@incollection(lit:neg,
 author       = {Tadeusz Litak and Miriam Polzer and Ulrich Rabenstein},
 year         = {2017},
 title        = {Negative translations and normal modality},
 booktitle    = {2nd {I}nternational {C}onference on {F}ormal {S}tructures for {C}omputation and {D}eduction},
 series       = {LIPIcs. Leibniz Int. Proc. Inform.},
 volume       = {84},
 publisher    = {Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern},
 pages        = {Art. No. 27, 18},
)
@book(lombardiquitte:constructive,
 author       = {Henri Lombardi and Claude Quitt\'e},
 year         = {2015},
 title        = {Commutative Algebra: Constructive Methods. Finite Projective Modules},
 series       = {Algebra and Applications},
 volume       = {20},
 publisher    = {Springer Netherlands},
 address      = {Dordrecht},
 doi          = {10.1007/978-94-017-9944-7},
)
@book(min:bib,
 author       = {Ray Mines and Fred Richman and Wim Ruitenburg},
 year         = {1988},
 title        = {{A Course in Constructive Algebra}},
 publisher    = {Springer},
 address      = {New York},
 doi          = {10.1007/978-1-4419-8640-5},
 note         = {Universitext},
)
@incollection(neg:sto,
 author       = {Sara Negri},
 year         = {1996},
 title        = {{Stone bases alias the constructive content of Stone representation}},
 editor       = {Aldo Ursini and Paolo Aglian{\`o}},
 booktitle    = {{Logic and algebra. Proceedings of the international conference dedicated to the memory of Roberto Magari, April 26--30, 1994, Pontignano, Italy}},
 series       = {Lecture {N}otes in {P}ure and {A}pplied {M}athematics},
 volume       = {180},
 publisher    = {Marcel Dekker},
 address      = {New York},
 pages        = {617--636},
 doi          = {10.1201/9780203748671-28},
)
@article(negri:cont,
 author       = {Sara Negri},
 year         = {2002},
 title        = {Continuous domains as formal spaces},
 journal      = {Math.~Structures Comput.~Sci.},
 volume       = {12},
 number       = {1},
 pages        = {19--52},
 doi          = {10.1017/S0960129501003450},
)
@article(negri:barr,
 author       = {Sara Negri},
 year         = {2003},
 title        = {Contraction-free sequent calculi for geometric theories with an application to {B}arr's theorem},
 journal      = {Arch.~Math.~Logic},
 volume       = {42},
 number       = {4},
 pages        = {389--401},
 doi          = {10.1007/s001530100124},
)
@article(neg:gli,
 author       = {Sara Negri},
 year         = {2016},
 title        = {Glivenko sequent classes in the light of structural proof theory},
 journal      = {Arch.~Math.~Logic},
 volume       = {55},
 number       = {3-4},
 pages        = {461--473},
 doi          = {10.1007/s00153-016-0474-y},
)
@article(neg:ord,
 author       = {Sara Negri and Jan von Plato and Thierry Coquand},
 year         = {2004},
 title        = {Proof-theoretical analysis of order relations},
 journal      = {Arch.~Math.~Logic},
 volume       = {43},
 pages        = {297--309},
 doi          = {10.1007/s00153-003-0209-8},
)
@book(spt,
 author       = {Sara Negri and {von Plato}, Jan},
 year         = {2001},
 title        = {Structural Proof Theory},
 publisher    = {Cambridge University Press},
 address      = {Cambridge},
 doi          = {10.1017/CBO9780511527340},
)
@book(neg:pa,
 author       = {Sara Negri and {von Plato}, Jan},
 year         = {2011},
 title        = {Proof Analysis. A Contribution to Hilbert's Last Problem},
 publisher    = {Cambridge University Press},
 address      = {Cambridge},
 doi          = {10.1017/CBO9781139003513},
)
@article(ono:gli,
 author       = {Hiroakira Ono},
 year         = {2009},
 title        = {Glivenko theorems revisited},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {161},
 number       = {2},
 pages        = {246--250},
 doi          = {10.1016/j.apal.2009.05.006},
)
@incollection(per:con,
 author       = {Luiz Carlos Pereira and Edward Hermann Haeusler},
 year         = {2015},
 title        = {On constructive fragments of classical logic},
 booktitle    = {Dag {P}rawitz on proofs and meaning},
 series       = {Outst. Contrib. Log.},
 volume       = {7},
 publisher    = {Springer, Cham},
 pages        = {281--292},
 doi          = {10.1007/978-3-319-11041-7_12},
)
@book(ras:alg,
 author       = {Helena Rasiowa},
 year         = {1974},
 title        = {{An Algebraic Approach to Non-Classical Logics.}},
 publisher    = {North-Holland Publishing Company},
 address      = {Amsterdam},
)
@book(restall:sub,
 author       = {Greg Restall},
 year         = {2000},
 title        = {An Introduction to Substructural Logics},
 publisher    = {Routledge},
 address      = {London},
 doi          = {10.4324/9780203252642},
)
@phdthesis(rin:phd,
 author       = {Davide Rinaldi},
 year         = {2014},
 title        = {Formal Methods in the Theories of Rings and Domains},
 type         = {Doctoral dissertation},
 school       = {Universit\"{a}t M\"{u}nchen},
)
@article(rin:edde,
 author       = {Davide Rinaldi and Peter Schuster and Daniel Wessel},
 year         = {2017},
 title        = {Eliminating disjunctions by disjunction elimination},
 journal      = {Bull.~Symb.~Logic},
 volume       = {23},
 number       = {2},
 pages        = {181--200},
 doi          = {10.1017/bsl.2017.13},
)
@article(rin:edde:full,
 author       = {Davide Rinaldi and Peter Schuster and Daniel Wessel},
 year         = {2018},
 title        = {Eliminating disjunctions by disjunction elimination},
 journal      = {Indag.~Math.~(N.S.)},
 volume       = {29},
 number       = {1},
 pages        = {226--259},
 doi          = {10.1016/j.indag.2017.09.011},
)
@article(rinwes:sik,
 author       = {Davide Rinaldi and Daniel Wessel},
 year         = {2018},
 title        = {Extension by conservation. {Sikorski's} theorem},
 journal      = {Log.~Methods Comput.~Sci.},
 volume       = {14},
 number       = {4:8},
 pages        = {1--17},
)
@article(rin:cuts,
 author       = {Davide Rinaldi and Daniel Wessel},
 year         = {2019},
 title        = {Cut elimination for entailment relations},
 journal      = {Arch. Math. Logic},
 volume       = {58},
 number       = {5--6},
 pages        = {605--625},
 doi          = {10.1007/s00153-018-0653-0},
)
@book(rosen,
 author       = {Kimmo I. Rosenthal},
 year         = {1990},
 title        = {Quantales and their Applications},
 series       = {Pitman Research Notes in Mathematics},
 volume       = {234},
 publisher    = {Longman Scientific \& Technical},
 address      = {Essex},
)
@incollection(sam:ifs,
 author       = {Giovanni Sambin},
 year         = {1987},
 title        = {{Intuitionistic formal spaces---a first communication}},
 editor       = {D. Skordev},
 booktitle    = {Mathematical Logic and its Applications, {P}roc. {A}dv. {I}nternat. {S}ummer {S}chool {C}onf., {D}ruzhba, {B}ulgaria, 1986},
 publisher    = {{Plenum}},
 address      = {New York},
 pages        = {187--204},
 doi          = {10.1007/978-1-4613-0897-3_12},
)
@article(sam:som,
 author       = {Giovanni Sambin},
 year         = {2003},
 title        = {Some points in formal topology},
 journal      = {Theoret.~Comput.~Sci.},
 volume       = {305},
 number       = {1--3},
 pages        = {347--408},
 doi          = {10.1016/S0304-3975(02)00704-1},
)
@book(sam:bas,
 author       = {Giovanni Sambin},
 year         = {{forthcoming}},
 title        = {The {B}asic {P}icture. {S}tructures for {C}onstructive {T}opology},
 series       = {{Oxford Logic Guides}},
 publisher    = {{Clarendon Press}},
 address      = {{Oxford}},
)
@article(sch:hah,
 author       = {Konstantin Schlagbauer and Peter Schuster and Daniel Wessel},
 year         = {2019},
 title        = {Der {S}atz von {Hahn--Banach} per {D}isjunktionselimination},
 journal      = {Confluentes Math.},
 volume       = {11},
 number       = {1},
 pages        = {79--93},
 doi          = {10.5802/cml.57},
)
@inproceedings(LICS2020,
 author       = {Peter Schuster and Daniel Wessel},
 year         = {2020},
 title        = {Resolving Finite Indeterminacy: A Definitive Constructive Universal Prime Ideal Theorem},
 booktitle    = {Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science},
 series       = {LICS \IeC{\textquoteright}20},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {820\IeC{\textendash}830},
 doi          = {10.1145/3373718.3394777},
)
@article(sco:eng,
 author       = {Dana Scott},
 year         = {1971},
 title        = {{On engendering an illusion of understanding}},
 journal      = {J.~Philos.},
 volume       = {68},
 pages        = {787--807},
 doi          = {10.2307/2024952},
)
@incollection(sco:com,
 author       = {Dana Scott},
 year         = {1974},
 title        = {Completeness and axiomatizability in many-valued logic},
 editor       = {Leon Henkin and John Addison and {C.C.} Chang and William Craig and Dana Scott and Robert Vaught},
 booktitle    = {Proceedings of the {T}arski {S}ymposium ({P}roc. {S}ympos. {P}ure {M}ath., {V}ol. {XXV}, {U}niv. {C}alifornia, {B}erkeley, {C}alif., 1971)},
 publisher    = {Amer. Math. Soc.},
 address      = {Providence, RI},
 pages        = {411--435},
 doi          = {10.1090/pspum/025/0363802},
)
@incollection(sco:bac,
 author       = {Dana S. Scott},
 year         = {1973},
 title        = {Background to formalization},
 editor       = {Hugues Leblanc},
 booktitle    = {Truth, syntax and modality ({P}roc. {C}onf. {A}lternative {S}emantics, {T}emple {U}niv., {P}hiladelphia, {P}a., 1970)},
 publisher    = {North-Holland, Amsterdam},
 pages        = {244--273. Studies in Logic and the Foundations of Math., Vol. 68},
 doi          = {10.1016/S0049-237X(08)71542-8},
)
@incollection(simm:frame,
 author       = {Harold Simmons},
 year         = {1978},
 title        = {A framework for topology},
 editor       = {Angus Macintyre and Leszek Pacholski and Jeff Paris},
 booktitle    = {Logic Colloquium '77},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {96},
 publisher    = {North-Holland Publishing Company},
 address      = {Amsterdam},
 pages        = {239--251},
 doi          = {10.1016/S0049-237X(08)72007-X},
)
@article(simm:cur,
 author       = {Harold Simmons},
 year         = {2010},
 title        = {A curious nucleus},
 journal      = {J. Pure Appl. Algebra},
 volume       = {214},
 pages        = {2063--2073},
 doi          = {10.1016/j.jpaa.2010.02.011},
)
@article(tarski:fundamental,
 author       = {Alfred Tarski},
 year         = {1930},
 title        = {Fundamentale {B}egriffe der {M}ethodologie der deduktiven {W}issenschaften.~{I}},
 journal      = {Monatsh.~Math.~Phys.},
 volume       = {37},
 pages        = {361--404},
 doi          = {10.1007/BF01696782},
)
@article(wang:lwd,
 author       = {San-min Wang and Petr Cintula},
 year         = {2008},
 title        = {Logics with disjunction and proof by cases},
 journal      = {Arch.~Math.~Logic},
 volume       = {47},
 number       = {5},
 pages        = {435--446},
 doi          = {10.1007/s00153-008-0088-0},
)
@article(doi:10.3166/jancl.18.341-364,
 author       = {Heinrich Wansing},
 year         = {2008},
 title        = {Constructive negation, implication, and co-implication},
 journal      = {Journal of Applied Non-Classical Logics},
 volume       = {18},
 number       = {2-3},
 pages        = {341--364},
 doi          = {10.3166/jancl.18.341-364},
)
@article(wes:ogc,
 author       = {Daniel Wessel},
 year         = {2019},
 title        = {Ordering groups constructively},
 journal      = {Comm.~Algebra},
 volume       = {47},
 number       = {12},
 pages        = {4853--4873},
 doi          = {10.1080/00927872.2018.1477947},
)
@incollection(wes:path,
 author       = {Daniel Wessel},
 year         = {2019},
 title        = {Point-free spectra of linear spreads},
 editor       = {S. Centrone and S. Negri and D. Sarikaya and P. Schuster},
 booktitle    = {{M}athesis {U}niversalis, {C}omputability and {P}roof},
 series       = {{S}ynthese {L}ibrary},
 publisher    = {Springer},
 pages        = {353--374},
 doi          = {10.1007/978-3-030-20447-1_19},
)