Typed Relational Conversion

Petr Lozov, Andrei Vyatkin, Dmitry Boulytchev

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

3 Scopus citations


We address the problem of transforming typed functional programs into relational form. In this form, a program can be run in various “directions” with some arguments left free, making it possible to acquire different behaviors from a single specification. We specify the syntax, typing rules and semantics for the source language as well as its relational extension, describe the conversion and prove its correctness both in terms of typing and dynamic semantics. We also discuss the limitations of our approach, present the implementation of the conversion for the subset of OCaml and evaluate it on a number of realistic examples.
Original languageEnglish
Title of host publicationTrends in Functional Programming
Subtitle of host publication18th International Symposium, TFP 2017, Canterbury, UK, June 19-21, 2017, Revised Selected Papers
PublisherSpringer Nature
Number of pages19
ISBN (Electronic)978-3-319-89719-6
ISBN (Print)978-3-319-89718-9
StatePublished - 19 Apr 2018
EventTrends in Functional Programming: 18th International Symposium - Canterbury, United Kingdom
Duration: 19 Jun 201721 Jun 2017

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Nature
ISSN (Print)0302-9743


ConferenceTrends in Functional Programming
Abbreviated titleTFP 2017
Country/TerritoryUnited Kingdom

Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


  • Relative Conversion
  • Relative Extension
  • Typing Rules
  • Hindley-Milner Type System
  • Disequality Constraints


Dive into the research topics of 'Typed Relational Conversion'. Together they form a unique fingerprint.

Cite this