License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SNAPL.2017.15
URN: urn:nbn:de:0030-drops-71346
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7134/
Go to the corresponding LIPIcs Volume Portal

Scherer, Gabriel

Search for Program Structure

pdf-format:
LIPIcs-SNAPL-2017-15.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{scherer:LIPIcs:2017:7134,
  author =	{Gabriel Scherer},
  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 =	{Benjamin S. Lerner and Rastislav Bod{\'i}k and Shriram Krishnamurthi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7134},
  URN =		{urn:nbn:de:0030-drops-71346},
  doi =		{10.4230/LIPIcs.SNAPL.2017.15},
  annote =	{Keywords: programs, proofs, focusing, canonicity}
}

Keywords: programs, proofs, focusing, canonicity
Collection: 2nd Summit on Advances in Programming Languages (SNAPL 2017)
Issue Date: 2017
Date of publication: 05.05.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI