3 Search Results for "Hern�ndez-Orallo, Jos�"


Document
The Call-By-Value Lambda-Calculus with Generalized Applications

Authors: José Espírito Santo

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)


Abstract
The lambda-calculus with generalized applications is the Curry-Howard counterpart to the system of natural deduction with generalized elimination rules for intuitionistic implicational logic. In this paper we identify a call-by-value variant of the system and prove confluence, strong normalization, and standardization. In the end, we show that the cbn and cbv variants of the system simulate each other via mappings based on extensions of the "protecting-by-a-lambda" compilation technique.

Cite as

José Espírito Santo. The Call-By-Value Lambda-Calculus with Generalized Applications. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 35:1-35:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{espiritosanto:LIPIcs.CSL.2020.35,
  author =	{Esp{\'\i}rito Santo, Jos\'{e}},
  title =	{{The Call-By-Value Lambda-Calculus with Generalized Applications}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{35:1--35:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.35},
  URN =		{urn:nbn:de:0030-drops-116786},
  doi =		{10.4230/LIPIcs.CSL.2020.35},
  annote =	{Keywords: Generalized applications, Natural deduction, Strong normalization, Standardization, Call-by-name, Call-by-value, Protecting-by-a-lambda}
}
Document
The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations

Authors: Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)


Abstract
We argue that European transport regulations can be formalized within the Sigma^1_1 fragment of monadic second order logic, and possibly weaker fragments including linear temporal logic. We consider several articles in the regulation to verify these claims.

Cite as

Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten. The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{dealmeidaborges_et_al:LIPIcs.TIME.2019.6,
  author =	{de Almeida Borges, Ana and Conejero Rodr{\'\i}guez, Juan Jos\'{e} and Fern\'{a}ndez-Duque, David and Gonz\'{a}lez Bedmar, Mireia and Joosten, Joost J.},
  title =	{{The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.6},
  URN =		{urn:nbn:de:0030-drops-113649},
  doi =		{10.4230/LIPIcs.TIME.2019.6},
  annote =	{Keywords: linear temporal logic, monadic second order logic, formalized law, transport regulations}
}
Document
Approaches and Applications of Inductive Programming (Dagstuhl Seminar 15442)

Authors: José Hernández-Orallo, Stephen H. Muggleton, Ute Schmid, and Benjamin Zorn

Published in: Dagstuhl Reports, Volume 5, Issue 10 (2016)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15442 "Approaches and Applications of Inductive Programming". After a short introduction to the state of the art to inductive programming research, an overview of the talks and the outcomes of discussion groups is given.

Cite as

José Hernández-Orallo, Stephen H. Muggleton, Ute Schmid, and Benjamin Zorn. Approaches and Applications of Inductive Programming (Dagstuhl Seminar 15442). In Dagstuhl Reports, Volume 5, Issue 10, pp. 89-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Article{hernandezorallo_et_al:DagRep.5.10.89,
  author =	{Hern\'{a}ndez-Orallo, Jos\'{e} and Muggleton, Stephen H. and Schmid, Ute and Zorn, Benjamin},
  title =	{{Approaches and Applications of Inductive Programming (Dagstuhl Seminar 15442)}},
  pages =	{89--111},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{10},
  editor =	{Hern\'{a}ndez-Orallo, Jos\'{e} and Muggleton, Stephen H. and Schmid, Ute and Zorn, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.10.89},
  URN =		{urn:nbn:de:0030-drops-57006},
  doi =		{10.4230/DagRep.5.10.89},
  annote =	{Keywords: inductive program synthesis, end-user programming, probabilistic programming, constraint programming, universal artificial intelligence, cognitive modeling}
}
  • Refine by Author
  • 1 Conejero Rodríguez, Juan José
  • 1 Espírito Santo, José
  • 1 Fernández-Duque, David
  • 1 González Bedmar, Mireia
  • 1 Hernández-Orallo, José
  • Show More...

  • Refine by Classification
  • 1 Applied computing → Law
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Lambda calculus
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Proof theory

  • Refine by Keyword
  • 1 Call-by-name
  • 1 Call-by-value
  • 1 Generalized applications
  • 1 Natural deduction
  • 1 Protecting-by-a-lambda
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2016
  • 1 2019
  • 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