1 Search Results for "Farka, Frantisek"


Document
Proof-Relevant Resolution for Elaboration of Programming Languages

Authors: Frantisek Farka

Published in: OASIcs, Volume 64, Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)


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.

Cite as

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)


Copy BibTex To Clipboard

@InProceedings{farka:OASIcs.ICLP.2018.18,
  author =	{Farka, Frantisek},
  title =	{{Proof-Relevant Resolution for Elaboration of Programming Languages}},
  booktitle =	{Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)},
  pages =	{18:1--18:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-090-3},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{64},
  editor =	{Dal Palu', Alessandro and Tarau, Paul and Saeedloei, Neda and Fodor, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2018.18},
  URN =		{urn:nbn:de:0030-drops-98848},
  doi =		{10.4230/OASIcs.ICLP.2018.18},
  annote =	{Keywords: resolution, elaboration, proof-relevant, dependent types, type classes}
}
  • Refine by Author
  • 1 Farka, Frantisek

  • Refine by Classification
  • 1 Theory of computation → Constraint and logic programming

  • Refine by Keyword
  • 1 dependent types
  • 1 elaboration
  • 1 proof-relevant
  • 1 resolution
  • 1 type classes

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2018

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