DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2024.28

Realizability Models for Large Cardinals

Authors: Laura Fontanella, Guillaume Geoffroy, and Richard Matthews

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract

Realizabilty is a branch of logic that aims at extracting the computational content of mathematical proofs by establishing a correspondence between proofs and programs. Invented by S.C. Kleene in the 1945 to develop a connection between intuitionism and Turing computable functions, realizability has evolved to include not only classical logic but even set theory, thanks to the work of J-L. Krivine. Krivine’s work made possible to build realizability models for Zermelo-Frænkel set theory, ZF, assuming its consistency. Nevertheless, a large part of set theoretic research involves investigating further axioms that are known as large cardinals axioms; in this paper we focus on four large cardinals axioms: the axioms of (strongly) inaccessible cardinal, Mahlo cardinals, measurable cardinals and Reinhardt cardinals. We show how to build realizability models for each of these four axioms assuming their consistency relative to ZFC or ZF.

Cite as

Laura Fontanella, Guillaume Geoffroy, and Richard Matthews. Realizability Models for Large Cardinals. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{fontanella_et_al:LIPIcs.CSL.2024.28,
  author =	{Fontanella, Laura and Geoffroy, Guillaume and Matthews, Richard},
  title =	{{Realizability Models for Large Cardinals}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.28},
  URN =		{urn:nbn:de:0030-drops-196715},
  doi =		{10.4230/LIPIcs.CSL.2024.28},
  annote =	{Keywords: Logic, Classical Realizability, Set Theory, Large Cardinals}
}

Document

DOI: 10.4230/LIPIcs.CSL.2021.23

A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations

Authors: Guillaume Geoffroy and Paolo Pistone

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract

Program semantics is traditionally concerned with program equivalence. However, in fields like approximate, incremental and probabilistic computation, it is often useful to describe to which extent two programs behave in a similar, although non equivalent way. This has motivated the study of program (pseudo)metrics, which have found widespread applications, e.g. in differential privacy. In this paper we show that the standard metric on real numbers can be lifted to higher-order types in a novel way, yielding a metric semantics of the simply typed lambda-calculus in which types are interpreted as quantale-valued partial metric spaces. Using such metrics we define a class of higher-order denotational models, called diameter space models, that provide a quantitative semantics of approximate program transformations. Noticeably, the distances between objects of higher-types are elements of functional, thus non-numerical, quantales. This allows us to model contextual reasoning about arbitrary functions, thus deviating from classic metric semantics.

Cite as

Guillaume Geoffroy and Paolo Pistone. A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{geoffroy_et_al:LIPIcs.CSL.2021.23,
  author =	{Geoffroy, Guillaume and Pistone, Paolo},
  title =	{{A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.23},
  URN =		{urn:nbn:de:0030-drops-134578},
  doi =		{10.4230/LIPIcs.CSL.2021.23},
  annote =	{Keywords: Simply typed \lambda-calculus, program metrics, approximate program transformations, partial metric spaces}
}

Search Results

Documents authored by Geoffroy, Guillaume

Realizability Models for Large Cardinals

Abstract

Cite as

A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations

Abstract

Cite as

Thanks for your feedback!

Could not send message