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.
@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.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} }
Feedback for Dagstuhl Publishing