PolyBar · A new approach to polymorphism through bar recursion

A new approach to polymorphism through bar recursion

"Some computer programs are blind to the kind of input they are given. The program taking an object ""a"" and returning the pair ""(a,a)"" is such an example: its code is the same regardless of whether ""a"" is an integer, a real number, a vector or even another program. A programming language is polymorphic if it allows the writting of such programs. The aim of the PolyBar project is to define and study a computational translation from a polymorphic programming language into a non-polymorphic language extended with the bar recursion operator: an operator implementing recursion over well-founded trees. The concepts underlying polymorphism and bar recursion being very different, this translation will allow the study of polymorphism with new tools coming from recursion theory. There exists connections involving the programming languages System F and System TBR and the mathematical theories Z2 and PA-AC: there is a curry-Howard correspondence between System F and Z2, a logical translation from Z2 to PA-AC, and a realizability interpretation of PA-AC into System TBR. The experienced researcher (ER) recently gave the first translation from System F to System TBR by composing these connections within a single framework. The PolyBar project aims at defining a direct computational translation from System F to System TBR, and exploiting it to give a new recursion-theoretic proof of termination of System F and unveil a connection between impredicativity and Zorn's lemma. The PolyBar project gives new insights on polymorphic programming, paving the way for new tools for producing safer software. Proving properties about polymorphic programs is a particularly difficult task. Conversely, simply-typed programming languages often enjoy properties that allows for more straightforward proofs of correctness. This method is more flexible and direct than that of reducibility candidates and properties about simply-typed programs are often easier to obtain than in the polymorphic case. The PolyBar project allows the extension of combinatorial techniques used in simply-typed languages to the polymorphic world. This will bring a new range of techniques for proving properties about polymorphic programs and promote the use of polymorphic languages in environments where safety is important. Formal proofs of computer software often require that the programmer works in a constrained programming language, ruling out polymorphism. The PolyBar project improves the state-of-the-art by extending the use of well-known proof techniques to polymorphic programming languages: computer programmers will be able to use the sophisticated features of polymorphism and still prove correctness properties on their programs."

Data: CORDIS, © European Union