2 Search Results for "Maietti, Maria Emilia"

Document
DOI: 10.4230/LIPIcs.TYPES.2018.6
Normalization by Evaluation for Typed Weak lambda-Reduction

Authors: Filippo Sestini

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
Weak reduction relations in the lambda-calculus are characterized by the rejection of the so-called xi-rule, which allows arbitrary reductions under abstractions. A notable instance of weak reduction can be found in the literature under the name restricted reduction or weak lambda-reduction. In this work, we attack the problem of algorithmically computing normal forms for lambda-wk, the lambda-calculus with weak lambda-reduction. We do so by first contrasting it with other weak systems, arguing that their notion of reduction is not strong enough to compute lambda-wk-normal forms. We observe that some aspects of weak lambda-reduction prevent us from normalizing lambda-wk directly, thus devise a new, better-behaved weak calculus lambda-ex, and reduce the normalization problem for lambda-w to that of lambda-ex. We finally define type systems for both calculi and apply Normalization by Evaluation to lambda-ex, obtaining a normalization proof for lambda-wk as a corollary. We formalize all our results in Agda, a proof-assistant based on intensional Martin-Löf Type Theory.
Cite as

Filippo Sestini. Normalization by Evaluation for Typed Weak lambda-Reduction. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{sestini:LIPIcs.TYPES.2018.6,
  author =	{Sestini, Filippo},
  title =	{{Normalization by Evaluation for Typed Weak lambda-Reduction}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.6},
  URN =		{urn:nbn:de:0030-drops-114101},
  doi =		{10.4230/LIPIcs.TYPES.2018.6},
  annote =	{Keywords: normalization, lambda-calculus, reduction, term-rewriting, Agda}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2014.162
An Extensional Kleene Realizability Semantics for the Minimalist Foundation

Authors: Maria Emilia Maietti and Samuele Maschio

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
We build a Kleene realizability semantics for the two-level Minimalist Foundation MF, ideated by Maietti and Sambin in 2005 and completed by Maietti in 2009. Thanks to this semantics we prove that both levels of MF are consistent with the formal Church Thesis CT. Since MF consists of two levels, an intensional one, called mtt, and an extensional one, called emtt, linked by an interpretation, it is enough to build a realizability semantics for the intensional level mtt to get one for the extensional one emtt, too. Moreover, both levels consists of type theories based on versions of Martin-Löf's type theory. Our realizability semantics for mtt is a modification of the realizability semantics by Beeson in 1985 for extensional first order Martin-Löf's type theory with one universe. So it is formalized in Feferman's classical arithmetic theory of inductive definitions, called ID1^. It is called extensional Kleene realizability semantics since it validates extensional equality of type-theoretic functions extFun, as in Beeson's one. The main modification we perform on Beeson's semantics is to interpret propositions, which are defined primitively in MF, in a proof-irrelevant way. As a consequence, we gain the validity of CT. Recalling that extFun+CT+AC are inconsistent over arithmetics with finite types, we conclude that our semantics does not validate the Axiom of Choice AC on generic types. On the contrary, Beeson's semantics does validate AC, being this a theorem of Martin-Löf's theory, but it does not validate CT. The semantics we present here seems to be the best approximation of Kleene realizability for the extensional level emtt. Indeed Beeson's semantics is not an option for emtt since AC on generic sets added to it entails the excluded middle.
Cite as

Maria Emilia Maietti and Samuele Maschio. An Extensional Kleene Realizability Semantics for the Minimalist Foundation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 162-186, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{maietti_et_al:LIPIcs.TYPES.2014.162,
  author =	{Maietti, Maria Emilia and Maschio, Samuele},
  title =	{{An Extensional Kleene Realizability Semantics for the Minimalist Foundation}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{162--186},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.162},
  URN =		{urn:nbn:de:0030-drops-54966},
  doi =		{10.4230/LIPIcs.TYPES.2014.162},
  annote =	{Keywords: Realizability, Type Theory, formal Church Thesis}
}
  • Refine by Author
  • 1 Maietti, Maria Emilia
  • 1 Maschio, Samuele
  • 1 Sestini, Filippo

  • Refine by Classification
  • 1 Theory of computation → Lambda calculus

  • Refine by Keyword
  • 1 Agda
  • 1 Realizability
  • 1 Type Theory
  • 1 formal Church Thesis
  • 1 lambda-calculus
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2015
  • 1 2019

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact