This development was started by Martin Escardo in 2010 as an svn
project, and
transferred to github
Monday 5th February 2018.
If you contribute, please add your full (legal or adopted) name and date at the place of contribution.
An html rendering of the Agda code is hosted at Martin Escardo's institutional web page.
You can use the following BibTeX entry to cite TypeTopology
:
@misc{type-topology,
title = {{TypeTopology}},
author = {Escard\'{o}, Mart\'{i}n H. and {contributors}},
url = {https://github.com/martinescardo/TypeTopology},
note = {{Agda} development},
}
If you are citing only your own files, then create a different bibtex file with only your name as author.
- source/index.lagda (only
--safe
modules). - source/AllModulesIndex.lagda (including "unsafe" ones).
- Each subdirectory in source/ has its own index file.
Please add yourself the first time you contribute.
- Alice Laroche
- Andrew Sneap
- Ayberk Tosun
- Brendan Hart
- Bruno Paiva
- Chuangjie Xu
- Cory Knapp
- Ettore Aldrovandi
- Fredrik Nordvall Forsberg
- Igor Arrieta (ii)
- Jon Sterling
- Keri D'Angelo
- Lane Biocini
- Marc Bezem
- Martin Escardo
- Nicolai Kraus
- Ohad Kammar
- Paul Levy (i)
- Paulo Oliva
- Peter Dybjer
- Simcha van Collem
- Thierry Coquand
- Todd Waugh Ambridge
- Tom de Jong
- Vincent Rahli
(i) These authors didn't write any single line of Agda code here, but they contributed to constructions, theorems and proofs via the hands of Martin Escardo.
(ii) These authors didn't write single line of Agda code here, but they contributed to constructions, theorems and proofs via the hands of Ayberk Tosun.
Publications resulting from TypeTopology
-
Martín H. Escardó. Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics. The Journal of Symbolic Logic, Volume 78 , Issue 3 , 2013 , pp. 764 - 784.
-
Martín H. Escardó. Continuity of Gödel's system T functionals via effectful forcing. Electronic Notes in Theoretical Computer Science, Volume 298, 2013, Pages 119-141. MFPS XXIX
-
Nicolai Kraus, Martín H. Escardó, T. Coquand, T. Altenkirch. Generalizations of Hedberg's Theorem. In: Hasegawa, M. (eds) Typed Lambda Calculi and Applications. TLCA 2013. Lecture Notes in Computer Science, vol 7941. Springer.
-
Martín H. Escardó. Constructive decidability of classical continuity. Mathematical Structures in Computer Science, Volume 25, Special Issue 7: Computing with Infinite Data: Topological and Logical Foundations Part 1, October 2015, pp. 1578 - 1589 DOI:
-
Martín H. Escardó and Chuangjie Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015).
-
Martín H. Escardó and T. Streicher. The intrinsic topology of Martin-Löf universes. Annals of Pure and Applied Logic, Volume 167, Issue 9, 2016, Pages 794-805.
-
Martín H. Escardó and Cory Knapp. Partial elements and recursion via dominances in univalent type theory. Leibniz International Proceedings in Informatics (LIPIcs), Proceedings of CSL 2017.
-
Nicolai Kraus, Martín H. Escardó, T. Coquand, T. Altenkirch. Notions of Anonymous Existence in Martin-Löf Type Theory. Logical Methods in Computer Science, March 24, 2017, Volume 13, Issue 1.
-
Tom de Jong. The Scott model of PCF in univalent type theory. Mathematical Structures in Computer Science, Volume 31, Issue 10 - Homotopy Type Theory 2019, July 2021.
-
Martín H. Escardó. The Cantor-Schröder-Bernstein Theorem for ∞-groupoids. Journal of Homotopy and Related Structures, 16(3), 363-366, 2021.
-
Martín H. Escardó. Injective types in univalent mathematics. Mathematical Structures in Computer Science, Volume 31 , Issue 1 , 2021 , pp. 89 - 111.
-
Tom de Jong and Martín H. Escardó. Domain Theory in Constructive and Predicative Univalent Foundations. Leibniz International Proceedings in Informatics (LIPIcs), Volume 183 - Proceedings of CSL 2021, January 2021.
-
Dan R. Ghica and Todd Waugh Ambridge. Global Optimisation with Constructive Reals. Logic in Computer Science (LICS), Proceedings of LICS 2021, June 2021.
-
Tom de Jong and Martín H. Escardó. Predicative Aspects of Order Theory in Univalent Foundations. Leibniz International Proceedings in Informatics (LIPIcs), Volume 195 - Proceedings of FSCD 2021, July 2021.
-
Ayberk Tosun and Martín H. Escardó. Patch Locale of a Spectral Locale in Univalent Type Theory. Electronic Notes in Theoretical Informatics and Computer Science, Volume 1 - Proceedings of MFPS XXXVIII, February 2023.
-
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu. Set-Theoretic and Type-Theoretic Ordinals Coincide. Logic in Computer Science (LICS), Proceedings of LICS 2023. June 2023.
https://doi.org/10.1109/LICS56636.2023.10175762
Publicly available at https://arxiv.org/abs/2301.10696.
-
Tom de Jong and Martín H. Escardó. On Small Types in Univalent Foundations. Logical Methods in Computer Science, Volume 19, Issue 2, May 2023.
-
Martín H. Escardó and Paulo Oliva. Higher-order Games with Dependent Types.
Theoretical Computer Science, Special issue "Continuity, Computability, Constructivity: From Logic to Algorithms", dedicated to Ulrich Berger's 65th birthday, volume 974, 29 September 2023, available online 2 August 2023.