2 Search Results for "de Vries, Gert-Jan"

Document
DOI: 10.4230/LIPIcs.ITP.2025.13
Barendregt’s Theory of the λ-Calculus, Refreshed and Formalized

Authors: Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Barendregt’s book on the untyped λ-calculus refines the inconsistent view of β-divergence as representation of the undefined via the key concept of head reduction. In this paper, we put together recent revisitations of some key theorems laid out in Barendregt’s book, and we formalize them in the Abella proof assistant. Our work provides a compact and refreshed presentation of the core of the book. The formalization faithfully mimics pen-and-paper proofs. Two interesting aspects are the manipulation of contexts for the study of contextual equivalence and a formal alternative to the informal trick at work in Takahashi’s proof of the genericity lemma. As a by-product, we obtain an alternative definition of contextual equivalence that does not mention contexts.
Cite as

Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs. Barendregt’s Theory of the λ-Calculus, Refreshed and Formalized. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lancelot_et_al:LIPIcs.ITP.2025.13,
  author =	{Lancelot, Adrienne and Accattoli, Beniamino and Vemclefs, Maxime},
  title =	{{Barendregt’s Theory of the \lambda-Calculus, Refreshed and Formalized}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{13:1--13:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.13},
  URN =		{urn:nbn:de:0030-drops-246114},
  doi =		{10.4230/LIPIcs.ITP.2025.13},
  annote =	{Keywords: lambda-calculus, head reduction, equational theory}
}
Document
DOI: 10.4230/DagSemProc.09081.4
Analysis of Robust Soft Learning Vector Quantization and an application to Facial Expression Recognition

Authors: Gert-Jan de Vries and Michael Biehl

Published in: Dagstuhl Seminar Proceedings, Volume 9081, Similarity-based learning on structures (2009)

Abstract
Learning Vector Quantization (LVQ) is a popular method for multiclass classification. Several variants of LVQ have been developed recently, of which Robust Soft Learning Vector Quantization (RSLVQ) is a promising one. Although LVQ methods have an intuitive design with clear updating rules, their dynamics are not yet well understood. In simulations within a controlled environment RSLVQ performed very close to optimal. This controlled environment enabled us to perform a mathematical analysis as a first step in obtaining a better theoretical understanding of the learning dynamics. In this talk I will discuss the theoretical analysis and its results. Moreover, I will focus on the practical application of RSLVQ to a real world dataset containing extracted features from facial expression data.
Cite as

Gert-Jan de Vries and Michael Biehl. Analysis of Robust Soft Learning Vector Quantization and an application to Facial Expression Recognition. In Similarity-based learning on structures. Dagstuhl Seminar Proceedings, Volume 9081, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{devries_et_al:DagSemProc.09081.4,
  author =	{de Vries, Gert-Jan and Biehl, Michael},
  title =	{{Analysis of Robust Soft Learning Vector Quantization and an application to Facial Expression Recognition}},
  booktitle =	{Similarity-based learning on structures},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9081},
  editor =	{Michael Biehl and Barbara Hammer and Sepp Hochreiter and Stefan C. Kremer and Thomas Villmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09081.4},
  URN =		{urn:nbn:de:0030-drops-20356},
  doi =		{10.4230/DagSemProc.09081.4},
  annote =	{Keywords: Learning Vector Quantization, Analysis, Facial Expression Recognition}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2009

  • Refine by Author
  • 1 Accattoli, Beniamino
  • 1 Biehl, Michael
  • 1 Lancelot, Adrienne
  • 1 Vemclefs, Maxime
  • 1 de Vries, Gert-Jan

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 DagSemProc

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

  • Refine by Keyword
  • 1 Analysis
  • 1 Facial Expression Recognition
  • 1 Learning Vector Quantization
  • 1 equational theory
  • 1 head reduction
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact