DROPS

Document

DOI: 10.4230/LIPIcs.SNAPL.2017.15

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.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

DOI: 10.4230/LIPIcs.TLCA.2015.317

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.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}
}

Search Results

Documents authored by Scherer, Gabriel

Search for Program Structure

Abstract

Cite as

Multi-Focusing on Extensional Rewriting with Sums

Abstract

Cite as

Thanks for your feedback!

Could not send message