DROPS

Found 2 Possible Name Variants:

Grienenberger, Emilie
Grienenberger, Émilie

Grienenberger, Emilie

Document

DOI: 10.4230/LIPIcs.TYPES.2022.4

Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory

Authors: Emilie Grienenberger

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract

Systems in which classical and intuitionistic logics coexist are called ecumenical. Such a system allows for interoperability and hybridization between classical and constructive propositions and proofs. We study Ecumenical STT, a theory expressed in the logical framework of the λΠ-calculus modulo theory. We prove soudness and conservativity of four subtheories of Ecumenical STT with respect to constructive and classical predicate logic and simple type theory. We also prove the weak normalization of well-typed terms and thus the consistency of Ecumenical STT.

Cite as

Emilie Grienenberger. Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{grienenberger:LIPIcs.TYPES.2022.4,
  author =	{Grienenberger, Emilie},
  title =	{{Expressing Ecumenical Systems in the \lambda\Pi-Calculus Modulo Theory}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.4},
  URN =		{urn:nbn:de:0030-drops-184479},
  doi =		{10.4230/LIPIcs.TYPES.2022.4},
  annote =	{Keywords: dependent types, predicate logic, higher order logic, constructivism, interoperability, ecumenical logics}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2021.20

Some Axioms for Mathematics

Authors: Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract

The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory.

Cite as

Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some Axioms for Mathematics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{blanqui_et_al:LIPIcs.FSCD.2021.20,
  author =	{Blanqui, Fr\'{e}d\'{e}ric and Dowek, Gilles and Grienenberger, \'{E}milie and Hondet, Gabriel and Thir\'{e}, Fran\c{c}ois},
  title =	{{Some Axioms for Mathematics}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.20},
  URN =		{urn:nbn:de:0030-drops-142581},
  doi =		{10.4230/LIPIcs.FSCD.2021.20},
  annote =	{Keywords: logical framework, axiomatic theory, dependent types, rewriting, interoperabilty}
}

Document

DOI: 10.4230/LIPIcs.ICDT.2019.24

Learning Definable Hypotheses on Trees

Authors: Emilie Grienenberger and Martin Ritzert

Published in: LIPIcs, Volume 127, 22nd International Conference on Database Theory (ICDT 2019)

Abstract

We study the problem of learning properties of nodes in tree structures. Those properties are specified by logical formulas, such as formulas from first-order or monadic second-order logic. We think of the tree as a database encoding a large dataset and therefore aim for learning algorithms which depend at most sublinearly on the size of the tree. We present a learning algorithm for quantifier-free formulas where the running time only depends polynomially on the number of training examples, but not on the size of the background structure. By a previous result on strings we know that for general first-order or monadic second-order (MSO) formulas a sublinear running time cannot be achieved. However, we show that by building an index on the tree in a linear time preprocessing phase, we can achieve a learning algorithm for MSO formulas with a logarithmic learning phase.

Cite as

Emilie Grienenberger and Martin Ritzert. Learning Definable Hypotheses on Trees. In 22nd International Conference on Database Theory (ICDT 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 127, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{grienenberger_et_al:LIPIcs.ICDT.2019.24,
  author =	{Grienenberger, Emilie and Ritzert, Martin},
  title =	{{Learning Definable Hypotheses on Trees}},
  booktitle =	{22nd International Conference on Database Theory (ICDT 2019)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-101-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{127},
  editor =	{Barcelo, Pablo and Calautti, Marco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2019.24},
  URN =		{urn:nbn:de:0030-drops-103261},
  doi =		{10.4230/LIPIcs.ICDT.2019.24},
  annote =	{Keywords: monadic second-order logic, trees, query learning}
}

Grienenberger, Émilie

Document

DOI: 10.4230/LIPIcs.TYPES.2022.4

Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory

Authors: Emilie Grienenberger

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract

Cite as

Copy BibTex To Clipboard

@InProceedings{grienenberger:LIPIcs.TYPES.2022.4,
  author =	{Grienenberger, Emilie},
  title =	{{Expressing Ecumenical Systems in the \lambda\Pi-Calculus Modulo Theory}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.4},
  URN =		{urn:nbn:de:0030-drops-184479},
  doi =		{10.4230/LIPIcs.TYPES.2022.4},
  annote =	{Keywords: dependent types, predicate logic, higher order logic, constructivism, interoperability, ecumenical logics}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2021.20

Some Axioms for Mathematics

Authors: Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract

Cite as

Copy BibTex To Clipboard

@InProceedings{blanqui_et_al:LIPIcs.FSCD.2021.20,
  author =	{Blanqui, Fr\'{e}d\'{e}ric and Dowek, Gilles and Grienenberger, \'{E}milie and Hondet, Gabriel and Thir\'{e}, Fran\c{c}ois},
  title =	{{Some Axioms for Mathematics}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.20},
  URN =		{urn:nbn:de:0030-drops-142581},
  doi =		{10.4230/LIPIcs.FSCD.2021.20},
  annote =	{Keywords: logical framework, axiomatic theory, dependent types, rewriting, interoperabilty}
}

Document

DOI: 10.4230/LIPIcs.ICDT.2019.24

Learning Definable Hypotheses on Trees

Authors: Emilie Grienenberger and Martin Ritzert

Published in: LIPIcs, Volume 127, 22nd International Conference on Database Theory (ICDT 2019)

Abstract

Cite as

Copy BibTex To Clipboard

@InProceedings{grienenberger_et_al:LIPIcs.ICDT.2019.24,
  author =	{Grienenberger, Emilie and Ritzert, Martin},
  title =	{{Learning Definable Hypotheses on Trees}},
  booktitle =	{22nd International Conference on Database Theory (ICDT 2019)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-101-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{127},
  editor =	{Barcelo, Pablo and Calautti, Marco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2019.24},
  URN =		{urn:nbn:de:0030-drops-103261},
  doi =		{10.4230/LIPIcs.ICDT.2019.24},
  annote =	{Keywords: monadic second-order logic, trees, query learning}
}

Search Results

Documents authored by Grienenberger, Émilie

Grienenberger, Emilie

Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory

Abstract

Cite as

Some Axioms for Mathematics

Abstract

Cite as

Learning Definable Hypotheses on Trees

Abstract

Cite as

Grienenberger, Émilie

Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory

Abstract

Cite as

Some Axioms for Mathematics

Abstract

Cite as

Learning Definable Hypotheses on Trees

Abstract

Cite as

Thanks for your feedback!

Could not send message