Document Open Access Logo

Search for Program Structure

Author Gabriel Scherer

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2017.15.pdf
  • Filesize: 438 kB
  • 14 pages

Document Identifiers

Author Details

Gabriel Scherer

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.SNAPL.2017.15

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.

Subject Classification

Keywords
  • programs
  • proofs
  • focusing
  • canonicity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3), 1992. Google Scholar
  2. Jean-Philippe Bernardy, Patrik Jansson, and Koen Claessen. Testing polymorphic properties. In ESOP, 2010. Google Scholar
  3. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR, 2010. Google Scholar
  4. Kaustuv Chaudhuri. Magically constraining the inverse method using dynamic polarity assignment. In LPAR, 2010. URL: https://hal.inria.fr/inria-00535948.
  5. Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. J. Autom. Reasoning, 40(2-3), 2008. Google Scholar
  6. Rowan Davies and Frank Pfenning. Intersection types and computational effects. In ICFP, 2000. Google Scholar
  7. Dominique Devriese, Marco Patrignani, and Frank Piessens. Fully abstract compilation by approximate back-translation. In POPL, 2016. Google Scholar
  8. Joshua Dunfield and Frank Pfenning. Tridirectional typechecking. In POPL, January 2004. Google Scholar
  9. Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, and Benjamin Livshits. Fully abstract compilation to JavaScript. In POPL, 2013. URL: http://research.microsoft.com/pubs/176601/js-star.pdf.
  10. Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic. Example-directed synthesis: a type-theoretic interpretation. In POPL, 2016. Google Scholar
  11. Neil Ghani. Beta-Eta Equality for Coproducts. In TLCA, 1995. Google Scholar
  12. Timothy G. Griffin. A formulae-as-type notion of control. In POPL, 1989. Google Scholar
  13. Alan Jeffrey. Ltl types frp: Linear-time temporal logic propositions as types, proofs as functional reactive programs. In PLPV, 2012. Google Scholar
  14. Olivier Laurent. Syntax vs. semantics: a polarized approach. Theoretical Computer Science, 343(1-2):177-206, 2005. Google Scholar
  15. Paul Blain Levy. Call-by-push-value: A subsuming paradigm. In TLCA, 1999. Google Scholar
  16. Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins. Monadic concurrent linear logic programming. In PPDP, 2005. Google Scholar
  17. Chris Martens. Ceptre: A language for modeling generative interactive systems. In AIIDE, 2015. Google Scholar
  18. Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 1991. Google Scholar
  19. Guillaume Munch-Maccagnoni. Focalisation and Classical Realisability. In CSL, 2009. Google Scholar
  20. Guillaume Munch-Maccagnoni. Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD thesis, Université Paris Diderot, 2013. Google Scholar
  21. Max S. New, William J. Bowman, and Amal Ahmed. Fully abstract compilation via universal embedding. In ICFP, 2016. Google Scholar
  22. Peter-Michael Osera and Steve Zdancewic. Type-and-example-directed program synthesis. In PLDI, 2015. Google Scholar
  23. Jennifer Paykin, Neelakantan R. Krishnaswami, and Steve Zdancewic. The essence of event-driven programming. In draft, 2016. Google Scholar
  24. Frank Pfenning. Partial polymorphic type inference and higher-order unification. In LFP, 1988. Google Scholar
  25. Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. Program synthesis from polymorphic refinement types. In PLDI, 2016. Google Scholar
  26. Anders Schack-Nielsen and Carsten Schürmann. Celf - A logical framework for deductive and concurrent systems (system description). In IJCAR, 2008. Google Scholar
  27. Gabriel Scherer. Mining opportunities for unique inhabitants in dependent programs. In DTP Workshop, 2013. Google Scholar
  28. Gabriel Scherer. Which types have a unique inhabitant? PhD thesis, Université Paris-Diderot, 2016. Google Scholar
  29. Gabriel Scherer. Deciding equivalence with sums and the empty type. In POPL, 2017. Google Scholar
  30. Gabriel Scherer and Didier Rémy. Which simple types have a unique inhabitant? In ICFP, 2015. Google Scholar
  31. Noam Zeilberger. On the unity of duality. Annals of Pure and Applied Logic, 2008. Google Scholar
  32. Noam Zeilberger. The Logical Basis of Evaluation Order and Pattern-Matching. PhD thesis, Carnegie Mellon University, 2009. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact