3 Search Results for "Scherer, Gabriel"


Document
Invited Talk
A Fresh Look at the lambda-Calculus (Invited Talk)

Authors: Beniamino Accattoli

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)


Abstract
The (untyped) lambda-calculus is almost 90 years old. And yet - we argue here - its study is far from being over. The paper is a bird’s eye view of the questions the author worked on in the last few years: how to measure the complexity of lambda-terms, how to decompose their evaluation, how to implement it, and how all this varies according to the evaluation strategy. The paper aims at inducing a new way of looking at an old topic, focussing on high-level issues and perspectives.

Cite as

Beniamino Accattoli. A Fresh Look at the lambda-Calculus (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{accattoli:LIPIcs.FSCD.2019.1,
  author =	{Accattoli, Beniamino},
  title =	{{A Fresh Look at the lambda-Calculus}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{1:1--1:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.1},
  URN =		{urn:nbn:de:0030-drops-105083},
  doi =		{10.4230/LIPIcs.FSCD.2019.1},
  annote =	{Keywords: lambda-calculus, sharing, abstract machines, type systems, rewriting}
}
Document
Search for Program Structure

Authors: Gabriel Scherer

Published in: LIPIcs, Volume 71, 2nd Summit on Advances in Programming Languages (SNAPL 2017)


Abstract
The community of programming language research loves the Curry-Howard correspondence between proofs and programs. Cut-elimination as computation, theorems for free, 'call/cc' as excluded middle, dependently typed languages as proof assistants, etc. Yet we have, for all these years, missed an obvious observation: "the structure of programs corresponds to the structure of proof search". For pure programs and intuitionistic logic, more is known about the latter than the former. We think we know what programs are, but logicians know better! To motivate the study of proof search for program structure, we retrace recent research on applying focusing to study the canonical structure of simply-typed lambda-terms. We then motivate the open problem of extending canonical forms to support richer type systems, such as polymorphism, by discussing a few enticing applications of more canonical program representations.

Cite as

Gabriel Scherer. Search for Program Structure. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{scherer:LIPIcs.SNAPL.2017.15,
  author =	{Scherer, Gabriel},
  title =	{{Search for Program Structure}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  pages =	{15:1--15:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-032-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{71},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.15},
  URN =		{urn:nbn:de:0030-drops-71346},
  doi =		{10.4230/LIPIcs.SNAPL.2017.15},
  annote =	{Keywords: programs, proofs, focusing, canonicity}
}
Document
Multi-Focusing on Extensional Rewriting with Sums

Authors: Gabriel Scherer

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)


Abstract
We propose a logical justification for the rewriting-based equivalence procedure for simply-typed lambda-terms with sums of Lindley. It relies on maximally multi-focused proofs, a notion of canonical derivations introduced for linear logic. Lindley’s rewriting closely corresponds to preemptive rewriting, a technical device used in the meta-theory of maximal multi-focus.

Cite as

Gabriel Scherer. Multi-Focusing on Extensional Rewriting with Sums. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 317-331, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{scherer:LIPIcs.TLCA.2015.317,
  author =	{Scherer, Gabriel},
  title =	{{Multi-Focusing on Extensional Rewriting with Sums}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{317--331},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.317},
  URN =		{urn:nbn:de:0030-drops-51721},
  doi =		{10.4230/LIPIcs.TLCA.2015.317},
  annote =	{Keywords: Maximal multi-focusing, extensional sums, rewriting, natural deduction}
}
  • Refine by Author
  • 2 Scherer, Gabriel
  • 1 Accattoli, Beniamino

  • Refine by Classification
  • 1 Software and its engineering → Functional languages
  • 1 Theory of computation → Lambda calculus
  • 1 Theory of computation → Operational semantics

  • Refine by Keyword
  • 2 rewriting
  • 1 Maximal multi-focusing
  • 1 abstract machines
  • 1 canonicity
  • 1 extensional sums
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2015
  • 1 2017
  • 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