@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},
)