Publication

On Complete Functional Synthesis

Abstract

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, synthesis algorithms should behave in a predictable way---they should succeed for a well-defined class of specifications. They should also support unbounded data types such as numbers and data structures. We propose to generalize decision procedures into predictable and complete synthesis procedures. Such procedures are guaranteed to find code that satisfies the specification if such code exists. Moreover, we identify conditions under which synthesis will statically decide whether the solution is guaranteed to exist, and whether it is unique. We demonstrate our approach by extending decision procedures for integer linear arithmetic and data structures into synthesis procedures, and establishing results on the size and the efficiency of the synthesized code. We show that such procedures are useful as a language extension with implicit value definitions, and we show how to extend a compiler to support such definitions. Our constructs provide the benefits of synthesis to programmers, without requiring them to learn new concepts or give up a deterministic execution model.

About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
Related concepts (37)
Programming language
A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming language is usually split into the two components of syntax (form) and semantics (meaning), which are usually defined by a formal language. Some languages are defined by a specification document (for example, the C programming language is specified by an ISO Standard) while other languages (such as Perl) have a dominant implementation that is treated as a reference.
Organic synthesis
Organic synthesis is a special branch of chemical synthesis and is concerned with the intentional construction of organic compounds. Organic molecules are often more complex than inorganic compounds, and their synthesis has developed into one of the most important branches of organic chemistry. There are several main areas of research within the general area of organic synthesis: total synthesis, semisynthesis, and methodology.
Peptide synthesis
In organic chemistry, peptide synthesis is the production of peptides, compounds where multiple amino acids are linked via amide bonds, also known as peptide bonds. Peptides are chemically synthesized by the condensation reaction of the carboxyl group of one amino acid to the amino group of another. Protecting group strategies are usually necessary to prevent undesirable side reactions with the various amino acid side chains. Chemical peptide synthesis most commonly starts at the carboxyl end of the peptide (C-terminus), and proceeds toward the amino-terminus (N-terminus).
Show more
Related publications (49)

Formal Foundations of Capture Tracking

Aleksander Slawomir Boruch-Gruszecki

Type systems are a device for verifying properties of programs without running them. Many programming languages used in the industry have always had a type system, while others were initially created without a type system and later adopted one, when the ad ...
EPFL2024

Dynamic Linkers Are the Narrow Waist of Operating Systems

Adrien Ghosn, Charly Nicolas Lucien Castes

While software applications, programming languages, and hardware have changed, operating systems have not. Widely-used commodity operating systems are still modeled after the ones designed in the seventies. The accumulated burden of backward compatibility ...
Association for Computing Machinery2023

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain

Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types ...
ASSOC COMPUTING MACHINERY2022
Show more
Related MOOCs (15)
Parallelism and Concurrency
(merge of parprog1, scala-reactive, scala-spark-big-data)
Functional Programming
In this course you will discover the elements of the functional programming style and learn how to apply them usefully in your daily programming tasks. You will also develop a solid foundation for rea
Functional Programming Principles in Scala [retired]
This advanced undergraduate programming course covers the principles of functional programming using Scala, including the use of functions as values, recursion, immutability, pattern matching, higher-
Show more