3 Search Results for "Oliva, Paulo"


Document
A Gentzen-Style Monadic Translation of Gödel’s System T

Authors: Chuangjie Xu

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)


Abstract
We introduce a syntactic translation of Gödel’s System 𝖳 parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzen’s negative translation of classical logic. By instantiating the monad and the logical relation, we reveal the well-known properties and structures of 𝖳-definable functionals including majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant.

Cite as

Chuangjie Xu. A Gentzen-Style Monadic Translation of Gödel’s System T. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{xu:LIPIcs.FSCD.2020.25,
  author =	{Xu, Chuangjie},
  title =	{{A Gentzen-Style Monadic Translation of G\"{o}del’s System T}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{25:1--25:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.25},
  URN =		{urn:nbn:de:0030-drops-123472},
  doi =		{10.4230/LIPIcs.FSCD.2020.25},
  annote =	{Keywords: monadic translation, G\"{o}del’s System T, logical relation, negative translation, majorizability, continuity, bar recursion, Agda}
}
Document
System T and the Product of Selection Functions

Authors: Martin Escardo, Paulo Oliva, and Thomas Powell

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)


Abstract
We show that the finite product of selection functions (for all finite types) is primitive recursively equivalent to Goedel's higher-type recursor (for all finite types). The correspondence is shown to hold for similar restricted fragments of both systems: The recursor for type level n+1 is primitive recursively equivalent to the finite product of selection functions of type level n. Whereas the recursor directly interprets induction, we show that other classical arithmetical principles such as bounded collection and finite choice are more naturally interpreted via the product of selection functions.

Cite as

Martin Escardo, Paulo Oliva, and Thomas Powell. System T and the Product of Selection Functions. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 233-247, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{escardo_et_al:LIPIcs.CSL.2011.233,
  author =	{Escardo, Martin and Oliva, Paulo and Powell, Thomas},
  title =	{{System T and the Product of Selection Functions}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{233--247},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.233},
  URN =		{urn:nbn:de:0030-drops-32341},
  doi =		{10.4230/LIPIcs.CSL.2011.233},
  annote =	{Keywords: primitive recursion, product of selection functions, finite choice, dialectica interpretation}
}
Document
Unifying Functional Interpretations

Authors: Paulo Oliva

Published in: Dagstuhl Seminar Proceedings, Volume 5021, Mathematics, Algorithms, Proofs (2006)


Abstract
The purpose of this article is to present a parametrised functional interpretation. Depending on the choice of the two parameters one obtains well-known functional interpretations, among others Gödel's Dialectica interpretation, Diller-Nahm's variant of the Dialectica interpretation, Kreisel's modified realizability, Kohlenbach's monotone interpretations and Stein's family of functional interpretations. We show that all these interpretations only differ on two basic choices, which are captured by the parameters, namely the choices of (1) "how much" of the counter-examples for A becomes witnesses for the negation of A, and of (2) "how much" information about the witnesses of A one is interested in.

Cite as

Paulo Oliva. Unifying Functional Interpretations. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{oliva:DagSemProc.05021.23,
  author =	{Oliva, Paulo},
  title =	{{Unifying Functional Interpretations}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5021},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05021.23},
  URN =		{urn:nbn:de:0030-drops-2919},
  doi =		{10.4230/DagSemProc.05021.23},
  annote =	{Keywords: Functional interpretation, modified realizability, Dialectica interpretation, intuitionistic logic}
}
  • Refine by Author
  • 2 Oliva, Paulo
  • 1 Escardo, Martin
  • 1 Powell, Thomas
  • 1 Xu, Chuangjie

  • Refine by Classification
  • 1 Theory of computation → Program analysis
  • 1 Theory of computation → Proof theory
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Agda
  • 1 Dialectica interpretation
  • 1 Functional interpretation
  • 1 Gödel’s System T
  • 1 bar recursion
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2006
  • 1 2011
  • 1 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail