Document Open Access Logo

Proof-Relevant Resolution for Elaboration of Programming Languages

Author Frantisek Farka

PDF
Thumbnail PDF

File

OASIcs.ICLP.2018.18.pdf
  • Filesize: 491 kB
  • 9 pages

Document Identifiers

Author Details

Frantisek Farka
  • University of St Andrews, UK, and, Heriot-Watt University, Edinburgh, UK

Cite AsGet BibTex

Frantisek Farka. Proof-Relevant Resolution for Elaboration of Programming Languages. In Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018). Open Access Series in Informatics (OASIcs), Volume 64, pp. 18:1-18:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/OASIcs.ICLP.2018.18

Abstract

Proof-relevant resolution is a new variant of resolution in Horn-clause logic and its extensions. We propose proof-relevant resolution as a systematic approach to elaboration in programming languages that is close to formal specification and hence allows for analysis of semantics of the language. We demonstrate the approach on two case studies; we describe a novel, proof-relevant approach to type inference and term synthesis in dependently types languages and we show how proof-relevant resolution allows for analysis of inductive and coinductive soundness of type class resolution. We conclude by a discussion of overall contributions of our current work.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • resolution
  • elaboration
  • proof-relevant
  • dependent types
  • type classes

Metrics

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

References

  1. Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program., 23(5):552-593, 2013. URL: http://dx.doi.org/10.1017/S095679681300018X.
  2. Dominique Devriese and Frank Piessens. On the bright side of type classes: instance arguments in Agda. In Proc. of ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 143-155, 2011. URL: http://dx.doi.org/10.1145/2034773.2034796.
  3. Frantisek Farka, Ekaterina Komendantskaya, and Kevin Hammond. Coinductive Soundness of Corecursive Type Class Resolution. In Manuel V. Hermenegildo and Pedro López-García, editors, Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, 2016, Revised Selected Papers, volume 10184 of Lecture Notes in Computer Science, pages 311-327. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-63139-4_18.
  4. František Farka, Ekaterina Komendantskaya, and Kevin Hammond. Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis. In accepted to ICLP 2018, 2018. Google Scholar
  5. Peng Fu and Ekaterina Komendantskaya. Operational semantics of resolution and productivity in Horn clause logic. Formal Asp. Comput., 29(3):453-474, 2017. URL: http://dx.doi.org/10.1007/s00165-016-0403-1.
  6. Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, and Andrew Pond. Proof Relevant Corecursive Resolution. In Oleg Kiselyov and Andy King, editors, Functional and Logic Programming - 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings, volume 9613 of Lecture Notes in Computer Science, pages 126-143. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-29604-3_9.
  7. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. How to make ad hoc proof automation less ad hoc. In Proc. of ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 163-175, 2011. URL: http://dx.doi.org/10.1145/2034773.2034798.
  8. Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip Wadler. Type Classes in Haskell. ACM Trans. Program. Lang. Syst., 18(2):109-138, 1996. URL: http://dx.doi.org/10.1145/227699.227700.
  9. Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log., 6(1):61-101, 2005. URL: http://dx.doi.org/10.1145/1042038.1042041.
  10. Georgios Karachalias and Tom Schrijvers. Elaboration on functional dependencies: functional dependencies are dead, long live functional dependencies! In Iavor S. Diatchki, editor, Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, Oxford, United Kingdom, September 7-8, 2017, pages 133-147. ACM, 2017. URL: http://dx.doi.org/10.1145/3122955.3122966.
  11. Ralf Lämmel and Simon L. Peyton Jones. Scrap your boilerplate with class: extensible generic functions. In Proc. of ICFP 2005, Tallinn, Estonia, September 26-28, 2005, pages 204-215, 2005. URL: http://dx.doi.org/10.1145/1086365.1086391.
  12. John W. Lloyd. Foundations of Logic Programming, 2nd Edition. Springer, 1987. Google Scholar
  13. Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, 1978. Google Scholar
  14. Simon Peyton Jones, Mark Jones, and Erik Meijer. Type classes: an exploration of the design space. In Haskell workshop, Amsterdam, January 1997. URL: https://www.microsoft.com/en-us/research/publication/type-classes-an-exploration-of-the-design-space/.
  15. Martin Sulzmann and Peter J. Stuckey. HM(X) type inference is CLP(X) solving. J. Funct. Program., 18(2):251-283, 2008. URL: http://dx.doi.org/10.1017/S0956796807006569.
  16. P. Wadler and S. Blott. How to Make Ad-hoc Polymorphism Less Ad Hoc. In Proc. of POPL '89, pages 60-76, New York, NY, USA, 1989. ACM. URL: http://dx.doi.org/10.1145/75277.75283.
  17. Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, and Richard A. Eisenberg. A specification for dependent types in Haskell. PACMPL, 1(ICFP):31:1-31:29, 2017. URL: http://dx.doi.org/10.1145/3110275.
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 Imprint Privacy Contact