Maria Emilia Maietti

Davide Trotta

Ann. Pure Appl. Log., April, 2023

A topological counterpart of well-founded trees in dependent type theory.

[BibT_eX]

[DOI]

Pietro Sabelli

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

2022

Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice.

[BibT_eX]

[DOI]

Michael Rathjen

Log. Methods Comput. Sci., 2022

2021

A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice.

[BibT_eX]

[DOI]

Michael Rathjen

Log. Methods Comput. Sci., 2021

A Predicative variant of Hyland's Effective Topos.

[BibT_eX]

[DOI]

J. Symb. Log., 2021

2019

Elementary Quotient Completions, Church's Thesis, and Partioned Assemblies.

[BibT_eX]

[DOI]

Fabio Pasquali

Giuseppe Rosolini

Log. Methods Comput. Sci., 2019

Preface to the special issue for The Fifth Workshop on Formal Topology.

[BibT_eX]

[DOI]

Thierry Coquand

Erik Palmgren

J. Log. Anal., 2019

2018

Consistency of the intensional level of the Minimalist Foundation with Church's thesis and axiom of choice.

[BibT_eX]

[DOI]

Arch. Math. Log., 2018

2017

On Choice Rules in Dependent Type Theory.

[BibT_eX]

[DOI]

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

2016

A Predicative Variant of a Realizability Tripos for the Minimalist Foundation.

[BibT_eX]

[DOI]

FLAP, 2016

Preface.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2016

2015

Unifying Exact Completions.

[BibT_eX]

[DOI]

Giuseppe Rosolini

Appl. Categorical Struct., 2015

2014

An Extensional Kleene Realizability Semantics for the Minimalist Foundation.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Types for Proofs and Programs, 2014

2013

Quotient Completion for the Foundation of Constructive Mathematics.

[BibT_eX]

[DOI]

Giuseppe Rosolini

Logica Universalis, 2013

Convergence in formal topology: a unifying notion.

[BibT_eX]

[DOI]

Francesco Ciraulo

Giovanni Sambin

J. Log. Anal., 2013

Constructive version of Boolean algebra.

[BibT_eX]

[DOI]

Francesco Ciraulo

Paola Toto

Log. J. IGPL, 2013

2011

Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita.

[BibT_eX]

[DOI]

Andrea Asperti

Claudio Sacerdoti Coen

Giovanni Sambin

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

2009

A minimalist two-level foundation for constructive mathematics.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2009

2007

Quotients over Minimal Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Computation and Logic in the Real World, 2007

2005

Modular correspondence between dependent type theories and categories including pretopoi and topoi.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2005

Relating Categorical Semantics for Intuitionistic Linear Logic.

[BibT_eX]

[DOI]

Appl. Categorical Struct., 2005

Toward a minimalistic foundation for constructive mathematics.

[BibT_eX]

Giovanni Sambin

Proceedings of the From sets and types to topology and analysis, 2005

Predicative exponentiation of locally compact formal topologies over inductively generated ones.

[BibT_eX]

Proceedings of the From sets and types to topology and analysis, 2005

2004

A structural investigation on formal topology: coreflection of formal covers and exponentiability.

[BibT_eX]

[DOI]

J. Symb. Log., 2004

Reflection Into Models of Finite Decidable FP-sketches in an Arithmetic Universe.

[BibT_eX]

[DOI]

Proceedings of the 10th Conference on Category Theory in Computer Science, 2004

2002

Exponentiation of Scott Formal Topologies.

[BibT_eX]

[DOI]

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

Joyal's arithmetic universes via type theory.

[BibT_eX]

[DOI]

Proceedings of the Category Theory and Computer Science, 2002

2000

Categorical Models for Intuitionistic and Linear Type Theory.

[BibT_eX]

[DOI]

Valeria de Paiva

Eike Ritter

Proceedings of the Foundations of Software Science and Computation Structures, 2000

1999

Can You Add Power-Sets to Martin-Löf's Intuitionistic Set Theory?

[BibT_eX]

[DOI]

Math. Log. Q., 1999

1998

About Effective Quotients in Constructive Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, 1998

1996

The Internal Type Theory of a Heyting Pretopos.

[BibT_eX]

[DOI]