License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.ICLP.2018.18
URN: urn:nbn:de:0030-drops-98848
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9884/
Go to the corresponding OASIcs Volume Portal

Farka, Frantisek

Proof-Relevant Resolution for Elaboration of Programming Languages

pdf-format:
OASIcs-ICLP-2018-18.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{farka:OASIcs:2018:9884,
  author =	{Frantisek Farka},
  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 =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-090-3},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{64},
  editor =	{Alessandro Dal Palu' and Paul Tarau and Neda Saeedloei and Paul Fodor},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9884},
  URN =		{urn:nbn:de:0030-drops-98848},
  doi =		{10.4230/OASIcs.ICLP.2018.18},
  annote =	{Keywords: resolution, elaboration, proof-relevant, dependent types, type classes}
}

Keywords: resolution, elaboration, proof-relevant, dependent types, type classes
Collection: Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)
Issue Date: 2018
Date of publication: 19.11.2018

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