TY - GEN
T1 - Search for program structure
AU - Scherer, Gabriel
N1 - Publisher Copyright:
© Gabriel Scherer; licensed under Creative Commons License CC-BY.
PY - 2017/5/1
Y1 - 2017/5/1
N2 - 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 γ-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.
AB - 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 γ-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.
KW - Canonicity
KW - Focusing
KW - Programs
KW - Proofs
U2 - 10.4230/LIPIcs.SNAPL.2017.15
DO - 10.4230/LIPIcs.SNAPL.2017.15
M3 - Conference contribution
AN - SCOPUS:85019649547
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 2nd Summit on Advances in Programming Languages, SNAPL 2017
A2 - Bodik, Rastislav
A2 - Lerner, Benjamin S.
A2 - Krishnamurthi, Shriram
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 2nd Summit on Advances in Programming Languages, SNAPL 2017
Y2 - 7 May 2017 through 10 May 2017
ER -