@incollection(AbramskyJung1995,
 author       = {S. Abramsky and A. Jung},
 year         = {1995},
 title        = {Domain Theory},
 editor       = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
 booktitle    = {Semantic Structures},
 series       = {Handbook of Logic in Computer Science},
 volume       = {3},
 publisher    = {Oxford University Press},
 pages        = {1--168},
 url          = {https://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf},
)
@phdthesis(Abramsky1987,
 author       = {Samson Abramsky},
 year         = {1987},
 title        = {Domain Theory and the Logic of Observable Properties},
 school       = {Queen Mary College, University of London},
)
@article(BauerKavkler2009,
 author       = {Andrej Bauer and Iztok Kavkler},
 year         = {2009},
 title        = {A constructive theory of continuous domains suitable for implementation},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {159},
 number       = {3},
 pages        = {251--267},
 doi          = {10.1016/j.apal.2008.09.025},
)
@inproceedings(BentonKennedyVarming2009,
 author       = {Nick Benton and Andrew Kennedy and Carsten Varming},
 year         = {2009},
 title        = {Some Domain Theory and Denotational Semantics in {Coq}},
 editor       = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
 booktitle    = {Theorem Proving in Higher Order Logics (TPHOLs 2009)},
 series       = {Lecture Notes in Computer Science},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {115--130},
 doi          = {10.1007/978-3-642-03359-9_10},
)
@book(BishopBridges1985,
 author       = {Errett Bishop and Douglas Bridges},
 year         = {1985},
 title        = {Constructive Analysis},
 series       = {Grundlehren der mathematischen Wissenschaften},
 volume       = {279},
 publisher    = {Springer-Verlag},
 doi          = {10.1007/978-3-642-61667-9},
)
@book(BridgesRichman1987,
 author       = {Douglas Bridges and Fred Richman},
 year         = {1987},
 title        = {Varieties of Constructive Mathematics},
 series       = {London Mathematical Society Lecture Note Series},
 volume       = {97},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/cbo9780511565663},
)
@book(BridgesVita2011,
 author       = {Douglas S. Bridges and V{\^{i}}{\c{t}}{\v{a}}, Lumini{\c{t}}a Simona},
 year         = {2011},
 title        = {Apartness and Uniformity: A Constructive Development},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-22415-7},
)
@article(CoquandEtAl2003,
 author       = {Thierry Coquand and Giovanni Sambin and Jan Smith and Silvio Valentini},
 year         = {2003},
 title        = {Inductively generated formal topologies},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {124},
 number       = {1--3},
 pages        = {71--106},
 doi          = {10.1016/s0168-0072(03)00052-6},
)
@inproceedings(Dockins2014,
 author       = {Robert Dockins},
 year         = {2014},
 title        = {{Formalized, Effective Domain Theory in Coq}},
 editor       = {Gerwin Klein and Ruben Gamboa},
 booktitle    = {Interactive Theorem Proving (ITP 2014)},
 series       = {Lecture Notes in Computer Science},
 volume       = {8558},
 publisher    = {Springer},
 pages        = {209--225},
 doi          = {10.1007/978-3-319-08970-6_14},
)
@article(Escardo2008,
 author       = {Martin Escardo},
 year         = {2008},
 title        = {Exhaustible sets in higher-type computation},
 journal      = {Logical Methods in Computer Science},
 volume       = {4},
 number       = {3},
 doi          = {10.2168/LMCS-4(3:3)2008},
)
@book(GierzEtAl2003,
 author       = {G. Gierz and K. H. Hofmann and K. Keimel and J. D. Lawson and M. Mislove and D. S. Scott},
 year         = {2003},
 title        = {Continuous Lattices and Domains},
 series       = {Encyclopedia of Mathematics and its Applications},
 volume       = {93},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511542725},
)
@unpublished(Heckmann1998,
 author       = {Reinhold Heckmann},
 year         = {1998},
 title        = {{Domain Environments}},
 url          = {https://www.rw.cdl.uni-saarland.de/people/heckmann/private/papers/newdomenv.ps.gz},
 note         = {Unpublished manuscript},
)
@article(Hedberg1996,
 author       = {Michael Hedberg},
 year         = {1996},
 title        = {{A type-theoretic interpretation of constructive domain theory}},
 journal      = {Journal of Automated Reasoning},
 volume       = {16},
 number       = {3},
 pages        = {369--425},
 doi          = {10.1007/BF00252182},
)
@inproceedings(Johnstone1984,
 author       = {Peter T. Johnstone},
 year         = {1984},
 title        = {Open locales and exponentiation},
 editor       = {J. W. Gray},
 booktitle    = {Mathematical Applications of Category Theory},
 series       = {Contemporary Mathematics},
 volume       = {30},
 publisher    = {American Mathematical Society},
 pages        = {84--116},
 doi          = {10.1090/conm/030/749770},
)
@inproceedings(deJongEscardo2021a,
 author       = {Tom de Jong and Mart{\'{i}}n H{\"{o}}tzel Escard{\'{o}}},
 year         = {2021},
 title        = {{Domain Theory in Constructive and Predicative Univalent Foundations}},
 editor       = {Christel Baier and Goubault-Larrecq, Jean},
 booktitle    = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {183},
 publisher    = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
 pages        = {28:1--28:18},
 doi          = {10.4230.LIPIcs.CSL.2021.28},
)
@inproceedings(deJongEscardo2021b,
 author       = {Tom de Jong and Mart{\'{i}}n H{\"{o}}tzel Escard{\'{o}}},
 year         = {2021},
 title        = {{Predicative Aspects of Order Theory in Univalent Foundations}},
 editor       = {Naoki Kobayashi},
 booktitle    = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {195},
 publisher    = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
 pages        = {8:1--8:18},
 doi          = {10.4230/LIPIcs.FSCD.2021.8},
)
@unpublished(Kawai2017,
 author       = {Tatsuji Kawai},
 year         = {2017},
 title        = {Geometric theories of patch and Lawson topologies},
 eprint       = {1709.06403},
)
@article(Kawai2021,
 author       = {Tatsuji Kawai},
 year         = {2021},
 title        = {Predicative theories of continuous lattices},
 journal      = {Logical Methods in Computer Science},
 volume       = {17},
 number       = {2},
 pages        = {22:1--22:38},
 doi          = {10.23638/LMCS-17(2:22)2021},
)
@article(Lawson1997,
 author       = {Jimmie Lawson},
 year         = {1997},
 title        = {Spaces of maximal points},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {7},
 number       = {5},
 pages        = {543--555},
 doi          = {10.1017/S0960129597002363},
)
@mastersthesis(Lidell2020,
 author       = {David Lidell},
 year         = {2020},
 title        = {{Formalizing domain models of the typed and the untyped lambda calculus in Agda}},
 school       = {{Chalmers University of Technology} and {University of Gothenburg}},
 url          = {https://hdl.handle.net/2077/67193},
)
@book(LongleyNormann2015,
 author       = {John Longley and Dag Normann},
 year         = {2015},
 title        = {Higher-Order Computability},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-47992-6},
)
@inproceedings(MaiettiValentini2004,
 author       = {Maria Emilia Maietti and Silvio Valentini},
 year         = {2004},
 title        = {Exponentiation of {Scott} Formal Topologies},
 editor       = {M. Escard{\'{o}}, A. Jung},
 booktitle    = {Proceedings of the Workshop on Domains VI},
 volume       = {73},
 pages        = {111--131},
 doi          = {10.1016/j.entcs.2004.08.005},
)
@book(MartinLof1970,
 author       = {Martin-L\"of, Per},
 year         = {1970},
 title        = {Notes on Constructive Mathematics},
 publisher    = {Almqvist and Wicksell},
 address      = {Stockholm},
)
@inproceedings(Negri1998,
 author       = {Sara Negri},
 year         = {1998},
 title        = {Continuous lattices in formal topology},
 editor       = {Eduardo Gim{\'{e}}nez and Paulin-Mohring, Christine},
 booktitle    = {{Types for Proofs and Programs (TYPES 1996)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {1512},
 publisher    = {Springer},
 pages        = {333--353},
 doi          = {10.1007/BFb0097800},
)
@article(Negri2002,
 author       = {Sara Negri},
 year         = {2002},
 title        = {Continuous domains as formal spaces},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {12},
 number       = {1},
 pages        = {19--52},
 doi          = {10.1017/S0960129501003450},
)
@article(PattinsonMohammadian2021,
 author       = {Dirk Pattinson and Mina Mohammadian},
 year         = {2021},
 title        = {Constructive Domains with Classical Witnesses},
 journal      = {Logical Methods in Computer Science},
 volume       = {17},
 number       = {1},
 pages        = {19:1--19:30},
 doi          = {10.23638/LMCS-17(1:19)2021},
)
@incollection(vonPlato2001,
 author       = {Jan von Plato},
 year         = {2001},
 title        = {Positive Lattices},
 editor       = {Peter Schuster and Ulrich Berger and Horst Osswald},
 booktitle    = {Reuniting the Antipodes --- Constructive and Nonstandard Views of the Continuum},
 series       = {Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science)},
 volume       = {306},
 publisher    = {Springer},
 pages        = {185--197},
 doi          = {10.1007/978-94-015-9757-9_16},
)
@article(Plotkin1977,
 author       = {G. D. Plotkin},
 year         = {1977},
 title        = {{LCF} considered as a programming language},
 journal      = {Theoretical Computer Science},
 volume       = {5},
 number       = {3},
 pages        = {223--255},
 doi          = {10.1016/0304-3975(77)90044-5},
)
@book(MinesRichmanRuitenburg1988,
 author       = {Ray Mines, Fred Richman and Wim Ruitenburg},
 year         = {1988},
 title        = {A Course in Constructive Algebra},
 publisher    = {Springer-Verlag},
 doi          = {10.1007/978-1-4419-8640-5},
)
@incollection(Sambin1987,
 author       = {Giovanni Sambin},
 year         = {1987},
 title        = {Intuitionistic formal spaces---a first communication},
 booktitle    = {Mathematical logic and its applications},
 publisher    = {Springer},
 pages        = {187--204},
 doi          = {10.1007/978-1-4613-0897-3_12},
)
@article(SambinValentiniVirgili1996,
 author       = {Giovanni Sambin and Silvio Valentini and Paolo Virgili},
 year         = {1996},
 title        = {Constructive domain theory as a branch of intuitionistic pointfree topology},
 journal      = {Theoretical Computer Science},
 volume       = {159},
 number       = {2},
 pages        = {319--341},
 doi          = {10.1016/0304-3975(95)00169-7},
)
@inproceedings(Scott1982,
 author       = {Dana S. Scott},
 year         = {1982},
 title        = {Lectures on a Mathematical Theory of Computation},
 editor       = {Manfred Broy and Gunther Schmidt},
 booktitle    = {Theoretical Foundations of Programming Methodology: Lecture Notes of an International Summer School, directed by F. L. Bauer, E. W. Dijkstra and C. A. R. Hoare},
 series       = {{NATO Advanced Study Institutes Series}},
 volume       = {91},
 publisher    = {Springer},
 pages        = {145--292},
 doi          = {10.1007/978-94-009-7893-5_9},
)
@article(Scott1993,
 author       = {Dana S. Scott},
 year         = {1993},
 title        = {A type-theoretical alternative to {ISWIM}, {CUCH}, {OWHY}},
 journal      = {Theoretical Computer Science},
 volume       = {121},
 number       = {1},
 pages        = {411--440},
 doi          = {10.1016/0304-3975(93)90095-B},
)
@incollection(Smyth1993,
 author       = {M. B Smyth},
 year         = {1993},
 title        = {Topology},
 editor       = {S. Abramsky and T. S. E. Maibaum},
 booktitle    = {Background: Mathematical Structures},
 series       = {Handbook of Logic in Computer Science},
 volume       = {1},
 publisher    = {Oxford University Press},
 pages        = {641--761},
)
@article(Smyth2006,
 author       = {Michael B. Smyth},
 year         = {2006},
 title        = {The constructive maximal point space and partial metrizability},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {137},
 number       = {1--3},
 pages        = {360--379},
 doi          = {10.1016/j.apal.2005.05.032},
)
@article(Spitters2010,
 author       = {Bas Spitters},
 year         = {2010},
 title        = {Locatedness and overt sublocales},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {162},
 number       = {1},
 pages        = {36--54},
 doi          = {10.1016/j.apal.2010.07.002},
)
@book(TroelstraVanDalen1988,
 author       = {A.S. Troelstra and D. van Dalen},
 year         = {1988},
 title        = {Constructivism in Mathematics: An Introduction (Volume II)},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {123},
 publisher    = {Elsevier Science Publishers},
)
@book(Vickers1989,
 author       = {Steven Vickers},
 year         = {1989},
 title        = {Topology via Logic},
 publisher    = {Cambridge University Press},
)