Martín Hötzel Escardó

CoRR, 2024

The Patch Topology in Univalent Foundations.

[BibT_eX]

[DOI]

Igor Arrieta

Ayberk Tosun

CoRR, 2024

2023

Higher-order games with dependent types.

[BibT_eX]

[DOI]

Theor. Comput. Sci., September, 2023

On Small Types in Univalent Foundations.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2023

Kreisel's counter-example to full abstraction of the set-theoretical model of Goedel's system T.

[BibT_eX]

[DOI]

CoRR, 2023

Patch Locale of a Spectral Locale in Univalent Type Theory.

[BibT_eX]

[DOI]

Ayberk Tosun

Proceedings of the 38th Conference on the Mathematical Foundations of Programming Semantics, 2023

2022

Type Theories with Universe Level Judgements.

[BibT_eX]

[DOI]

CoRR, 2022

Type Theory with Explicit Universe Polymorphism.

[BibT_eX]

[DOI]

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

2021

Injective types in univalent mathematics.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2021

On generalized algebraic theories and categories with families.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2021

Size Matters in Univalent Foundations.

[BibT_eX]

[DOI]

CoRR, 2021

Predicative Aspects of Order Theory in Univalent Foundations.

[BibT_eX]

[DOI]

Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction, 2021

Domain Theory in Constructive and Predicative Univalent Foundations.

[BibT_eX]

[DOI]

Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

2020

A Note on Generalized Algebraic Theories and Categories with Families.

[BibT_eX]

[DOI]

CoRR, 2020

2019

Introduction to Univalent Foundations of Mathematics with Agda.

[BibT_eX]

[DOI]

CoRR, 2019

2018

Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341).

[BibT_eX]

[DOI]

Andrej Bauer

Peter LeFanu Lumsdaine

Assia Mahboubi

Dagstuhl Reports, 2018

2017

The Herbrand Functional Interpretation of the double Negation Shift.

[BibT_eX]

[DOI]

J. Symb. Log., 2017

Notions of Anonymous Existence in Martin-Löf Type Theory.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2017

Partial Elements and Recursion via Dominances in Univalent Type Theory.

[BibT_eX]

[DOI]

Cory M. Knapp

Proceedings of the 26th EACSL Annual Conference on Computer Science Logic, 2017

2016

A constructive manifestation of the Kleene-Kreisel continuous functionals.

[BibT_eX]

[DOI]

Chuangjie Xu

Ann. Pure Appl. Log., 2016

The intrinsic topology of Martin-Löf universes.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2016

Parametricity, Automorphisms of the Universe, and Excluded Middle.

[BibT_eX]

[DOI]

Auke Bart Booij

Peter LeFanu Lumsdaine

Michael Shulman

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

2015

Constructive decidability of classical continuity.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2015

Bar Recursion and Products of Selection Functions.

[BibT_eX]

[DOI]

J. Symb. Log., 2015

Preface.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2015

The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard Interpretation.

[BibT_eX]

[DOI]

Chuangjie Xu

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

2014

Abstract Datatypes for Real Numbers in Type Theory.

[BibT_eX]

[DOI]

Alex Simpson

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

2013

Algorithmic solution of higher type equations.

[BibT_eX]

[DOI]

J. Log. Comput., 2013

Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics.

[BibT_eX]

[DOI]

J. Symb. Log., 2013

Continuity of Gödel's System T Definable Functionals via Effectful Forcing.

[BibT_eX]

[DOI]

Proceedings of the Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics, 2013

A Constructive Model of Uniform Continuity.

[BibT_eX]

[DOI]

Chuangjie Xu

Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

Generalizations of Hedberg's Theorem.

[BibT_eX]

[DOI]

Nicolai Kraus

Thierry Coquand

Thorsten Altenkirch

Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

2012

The Peirce translation.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2012

Computing Nash Equilibria of Unbounded Games.

[BibT_eX]

[DOI]

Proceedings of the Turing-100, 2012

2011

System T and the Product of Selection Functions.

[BibT_eX]

[DOI]

Thomas Powell

Proceedings of the Computer Science Logic, 2011

2010

Selection functions, bar recursion and backward induction.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2010

What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift Have in Common.

[BibT_eX]

[DOI]

Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, 2010

The Peirce Translation and the Double Negation Shift.

[BibT_eX]

[DOI]

Proceedings of the Programs, Proofs, Processes, 6th Conference on Computability in Europe, 2010

Computational Interpretations of Analysis via Products of Selection Functions.

[BibT_eX]

[DOI]

Proceedings of the Programs, Proofs, Processes, 6th Conference on Computability in Europe, 2010

2009

Operational domain theory and topology of sequential programming languages.

[BibT_eX]

[DOI]

Weng Kin Ho

Inf. Comput., 2009

Semi-decidability of May, Must and Probabilistic Testing in a Higher-type Setting.

[BibT_eX]

[DOI]

Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics, 2009

Computability of Continuous Solutions of Higher-Type Equations.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Theory and Computational Practice, 2009

Theory and Practice of Higher-type Computation (Tutorial).

[BibT_eX]

[DOI]

Proceedings of the Sixth International Conference on Computability and Complexity in Analysis, 2009

2008

Exhaustible Sets in Higher-type Computation.

[BibT_eX]

[DOI]

José Raymundo Marcial-Romero

Log. Methods Comput. Sci., 2008

2007

Semantics of a sequential language for exact real-number computation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2007

Infinite sets that admit fast exhaustive search.

[BibT_eX]

[DOI]

Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

2006

On the computational content of the Lawson topology.

[BibT_eX]

[DOI]

Frédéric De Jaeger

Gabriele Santini

Theor. Comput. Sci., 2006

Preface.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2006

Compactly generated Hausdorff locales.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2006

The Extended Probabilistic Powerdomain Monad over Stably Compact Spaces.

[BibT_eX]

[DOI]

Ben Cohen

Klaus Keimel

Proceedings of the Theory and Applications of Models of Computation, 2006

2005

Guest editors' introduction: Special issue on practical development of exact real number computation.

[BibT_eX]

[DOI]

Norbert Th. Müller

Paul Zimmermann

J. Log. Algebraic Methods Program., 2005

Preface.

[BibT_eX]

[DOI]

Michael W. Mislove

Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics, 2005

Operational Domain Theory and Topology of a Sequential Programming Language.

[BibT_eX]

[DOI]

Weng Kin Ho

Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

Compactness in Topology and Computation.

[BibT_eX]

Proceedings of the CCA 2005, 2005

2004

Preface: Recent Developments in Domain Theory: A collection of papers in honour of Dana S. Scott.

[BibT_eX]

[DOI]

Lars Birkedal

Giuseppe Rosolini

Theor. Comput. Sci., 2004

On the non-sequential nature of the interval-domain model of real-number computation.

[BibT_eX]

[DOI]

Martin Hofmann

Math. Struct. Comput. Sci., 2004

2003

Preface.

[BibT_eX]

[DOI]

Jirí Adámek

Martin Hofmann

Theor. Comput. Sci., 2003

Synthetic Topology: of Data Types and Classical Spaces.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Domain Theoretic Methods for Probabilistic Processes, 2003

Joins in the Frame of Nuclei.

[BibT_eX]

[DOI]

Appl. Categorical Struct., 2003

2002

In Domain Realizability, not all Functionals on <i>C</i>[-1, 1] are Continuous.

[BibT_eX]

[DOI]

Math. Log. Q., 2002

Preface.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Domains VI 2002, Birmingham, UK, September 16-19, 2002, 2002

Comparing Functional Paradigms for Exact Real-Number Computation.

[BibT_eX]

[DOI]

Andrej Bauer

Alex K. Simpson

Proceedings of the Automata, Languages and Programming, 29th International Colloquium, 2002

2001

A Universal Characterization of the Closed Euclidean Interval.

[BibT_eX]

[DOI]

Alex K. Simpson

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000

Integration in Real PCF.

[BibT_eX]

[DOI]

Abbas Edalat

Inf. Comput., 2000

Hausdorff compactifications of topological function spaces via the theory of continuous lattices.

[BibT_eX]

[DOI]

Proceedings of the First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, 2000

1999

Induction and Recursion on the Partial Real Line with Applications to Real PCF.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1999

Semantic Domains, Injective Spaces and Monads.

[BibT_eX]

[DOI]

Bob Flagg

Proceedings of the Fifteenth Conference on Mathematical Foundations of Progamming Semantics, 1999

On the Compact-regular Coreflection of a Stably Locally Compact Locale.

[BibT_eX]

[DOI]

Proceedings of the Fifteenth Conference on Mathematical Foundations of Progamming Semantics, 1999

1998

Calculus in Coinductive Form.

[BibT_eX]

[DOI]

Dusko Pavlovic

Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

1997

PCF extended with real numbers : a domain-theoretic approach to higher-order exact real number computation.

[BibT_eX]

[DOI]

PhD thesis, 1997

Effective and sequential definition by cases on the reals via infinite signed-digit numerals.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Computation and Approximation, 1997

Semantics of Exact Real Arithmetic.

[BibT_eX]

[DOI]

Peter John Potts

Abbas Edalat

Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997

Induction and Recursion on the Partial Real Line via Biquotients of Bifree Algebras.

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997

1996

PCF Extended with Real Numbers.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1996

1994

Recursion and Induction on the Real Line.

[BibT_eX]

Proceedings of the Proceedings for the Second Imperial College Department of Computing Workshop on Theory and Formal Methods, 1994

1993

On lazy natural numbers with applications to computability theory and functional programming.

[BibT_eX]

[DOI]