Search

Syntactic sugar refers to a certain syntactic structure added to the programming language. This syntactic structure has no effect on the function of the language, but is more convenient for programmers to use. Since syntactic sugar will be translated to the basic syntactic structure of the core language at the compilation stage, the relationship between the source program written with syntactic sugar and the execution of the core program is masked, and the compiled program is unfamiliar to programmers. It is not convenient for programmers to learn and debug source programs written with syntactic sugar. To solve that problem, this paper adopts the idea of resugaring for automatically transforming the evaluation sequence of the core language into the evaluation sequence of the surface language, and gives a cheap implementation using the existing bidirectional transformation tool BIRDS. The resugaring algorithms for both non-recursive and recursive desugaring transformations are implemented using Datalog, and the solutions to maintain two important properties of emulation and abstraction in the process of resugaring are studied.

The emergence of heterogeneous processors such as GPUs provide massively parallel computing power but also exacerbate the difficulties of parallel programming. Although low-level programming methods such as CUDA and OpenCL can yield good performance, the programming productivity is poor and applications lack portability. In this paper, we present a core language Ruler, which extends C with high-level parallel constructs. These constructs enable programmers to express parallelism in programs without concerning runtime details, thus ease user programming. We present the operational semantics of the language and show how these constructs reserve parallel patterns and parallelism degree of high-level applications. Those information could inform the compiler to generate efficient code and maintain the performance on different platforms. We have implemented a compiler and runtime system for Ruler on the top of OpenCL. Multiple benchmarks are rebuilt with Ruler and evaluated on both a NVIDIA GPU and an Intel MIC platform to demonstrate the effectiveness of our techniques. The size of Ruler code is only 13%-64% to that of the OpenCL code. The rebuilt benchmarks execute smoothly on both platforms after compilation, yielding a competitive performance to that of handcrafted benchmark OpenCL code on both platforms.

Geometric folding processes are ubiquitous in natural systems ranging from protein biochemistry to patterns of insect wings and leaves. In a previous study, a folding operation between strings of formal languages was introduced as a model of such processes. The operation was then used to define a folding system (F-system) as a construct consisting of a core language, containing the strings to be folded, and a folding procedure language, which defines how the folding is done. This paper reviews main definitions associated with F-systems and next it determines necessary conditions for a language to belong to classes generated by such systems. The conditions are stated in the form of pumping lemmas and four classes are considered, in which the core and folding procedure languages are both regular, one of them is regular and the other context-free, or both are context-free. Full demonstrations of the lemmas are provided, and the analysis is illustrated with examples., 12 pages, 6 figures. This is a preprint (pre-refereeing) version of a manuscript accepted for publication in Natural Computing

System F, also known as the polymorphic \(\lambda \)-calculus, is a typed \(\lambda \)-calculus independently discovered by the logician Jean-Yves Girard and the computer scientist John Reynolds. We consider \(F_{\omega \mu }\), which adds higher-order kinds and iso-recursive types. We present the first complete, intrinsically typed, executable, formalisation of System \(F_{\omega \mu }\) that we are aware of. The work is motivated by verifying the core language of a smart contract system based on System \(F_{\omega \mu }\). The paper is a literate Agda script [14].

Many programming languages and proof assistants are defined by elaboration from a high-level language with a great deal of implicit information to a highly explicit core language. In many advanced languages, these elaboration facilities contain powerful tools for program construction, but these tools are rarely designed to be repurposed by users. We describe elaborator reflection , a paradigm for metaprogramming in which the elaboration machinery is made directly available to metaprograms, as well as a concrete realization of elaborator reflection in Idris, a functional language with full dependent types. We demonstrate the applicability of Idris’s reflected elaboration framework to a number of realistic problems, we discuss the motivation for the specific features of its design, and we explore the broader meaning of elaborator reflection as it can relate to other languages.

We present a higher-order module system for the purely functional data-parallel array language Futhark. The module language has the property that it is completely eliminated at compile time, yet it serves as a powerful tool for organizing libraries and complete programs. The presentation includes a static and a dynamic semantics for the language in terms of, respectively, a static type system and a provably terminating elaboration of terms into terms of an underlying target language. The development is formalised in Coq using a novel encoding of semantic objects based on products, sets, and finite maps. The module language features a unified treatment of module type abstraction and core language polymorphism and is rich enough for expressing practical forms of module composition.

This paper aims to foster cross-fertilisation between programming language and compiler research performed on different array programming language infrastructures. We study how to enable better comparability of concepts and techniques by looking into generic translations between array languages. Our approach is based on the idea of a basic core language Heh which only captures the absolute essentials of array languages: multi-dimensional arrays and shape-invariant operations on them. Subsequently, we investigate how to map these constructs into several existing languages: SaC, APL, Julia, Python, and C. This approach provides us with some first understanding on how the peculiarities of these languages affect their suitability for expressing the basic building-blocks of array languages. We show that the existing tool-chains by-and-large are very sensitive to the way code is specified. Furthermore, we expose several fundamental programming patterns where optimisations missing in one or the other tool chain inhibit fair comparisons and, with it, cross-fertilisation.

This paper presents \(\mathsf {CoreFun}\), a typed reversible functional language, which seeks to reduce typed reversible functional programming to its essentials. We present a complete formal definition of the language, including its formal semantics and type system, the latter of which is based on a combined reasoning logical system of unrestricted and relevantly typed terms, and allows special support for ancillary (read-only) variables through its unrestricted fragment. We show how, in many cases, the type system provides the possibility to statically check for the reversibility of programs. Finally, we detail how higher-level language features such as variants and type classes may be incorporated into \(\mathsf {CoreFun}\) as syntactic sugar, such that \(\mathsf {CoreFun}\) may be used as a core language for a reversible functional language in a more modern style.

In response to the challenges associated with a Coq-based extraction of readable and traceable Scala code, the Scallina project defines a grammar delimiting a common subset of Gallina and Scala along with an optimized translation strategy for programs conforming to the aforementioned grammar. The Scallina translator shows how these contributions can be transferred into a working prototype. A typical application features a user implementing a functional program in Gallina, the core language of Coq, proving this program’s correctness with regards to its specification and making use of Scallina to synthesize readable Scala components.

Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is hard. In essence, the problem is that dependent type systems are designed around high-level compositional abstractions to decide type checking, but compilation interferes with the type-system rules for reasoning about run-time terms. We develop a type-preserving closure-conversion translation from the Calculus of Constructions (CC) with strong dependent pairs (Σ types)—a subset of the core language of Coq—to a type-safe, dependently typed compiler intermediate language named CC-CC. The central challenge in this work is how to translate the source type-system rules for reasoning about functions into target type-system rules for reasoning about closures. To justify these rules, we prove soundness of CC-CC by giving a model in CC. In addition to type preservation, we prove correctness of separate compilation.

This paper presents the Scallina prototype: a new tool which allows the translation of verified Coq programs to Scala. A typical workflow features a user implementing a functional program in Gallina, the core language of Coq, proving this program’s correctness with regards to its specification and making use of Scallina to synthesize readable Scala components.

As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an ML-like language with native support for handlers, has a subtyping-based effect system on which an effectaware optimizing compiler could be built. Unfortunately, in our experience, implementing optimizations for Eff is overly error-prone because its core language is implicitly-typed, making code transformations very fragile. To remedy this, we present an explicitly-typed polymorphic core calculus for algebraic effect handlers with a subtyping-based type-and-effect system. It reifies appeals to subtyping in explicit casts with coercions that witness the subtyping proof, quickly exposing typing bugs in program transformations. Our typing-directed elaboration comes with a constraint-based inference algorithm that turns an implicitly-typed Eff-like language into our calculus. Moreover, all coercions and effect information can be erased in a straightforward way, demonstrating that coercions have no computational content. ispartof: pages:327-354 ispartof: Lecture Notes in Computer Science vol:10801 pages:327-354 ispartof: European Symposium on Programming location:Thessaloniki, Greece date:14 Apr - 20 Apr 2018 status: Published online

A commonly used approach to develop parallel programs is to augment a sequential program with compiler directives that indicate which program blocks may potentially be executed in parallel. This paper develops a verification technique to prove correctness of compiler directives combined with functional correctness of the program. We propose syntax and semantics for a simple core language, capturing the main forms of deterministic parallel programs. This language distinguishes three kinds of basic blocks: parallel, vectorized and sequential blocks, which can be composed using three different composition operators: sequential, parallel and fusion composition. We show that it is sufficient to have contracts for the basic blocks to prove correctness of the compiler directives, and moreover that functional correctness of the sequential program implies correctness of the parallelized program. We formally prove correctness of our approach. In addition, we define a widely-used subset of OpenMP that can be encoded into our core language, thus effectively enabling the verification of OpenMP compiler directives, and we discuss automated tool support for this verification process.

Our goal is to create a convenient natural language interface for performing well-specified but complex actions such as analyzing data, manipulating text, and querying databases. However, existing natural language interfaces for such tasks are quite primitive compared to the power one wields with a programming language. To bridge this gap, we start with a core programming language and allow users to "naturalize" the core language incrementally by defining alternative, more natural syntax and increasingly complex concepts in terms of compositions of simpler ones. In a voxel world, we show that a community of users can simultaneously teach a common system a diverse language and use it to build hundreds of complex voxel structures. Over the course of three days, these users went from using only the core language to using the naturalized language in 85.9\% of the last 10K utterances., 10 pages, ACL2017

Let Γ be a set of rational-valued functions on a fixed finite domain; such a set is called a finite-valued constraint language. The valued constraint satisfaction problem, VCSP(Γ), is the problem of minimising a function given as a sum of functions from Γ. We establish a dichotomy theorem with respect to exact solvability for all finite-valued languages defined on domains of arbitrary finite size. We show that every core language Γ either admits a binary idempotent and symmetric fractional polymorphism in which case the basic linear programming relaxation solves any instance of VCSP(Γ) exactly, or Γ satisfies a simple hardness condition that allows for a polynomial-time reduction from Max-Cut to VCSP(Γ). In other words, there is a single algorithm for all tractable cases and a single reason for intractability. Our results show that for exact solvability of VCSPs the basic linear programming relaxation suffices and semidefinite relaxations do not add any power. The proof uses a variation of Motzkin’s Transposition Theorem, hyperplane arrangements, and a technique recently introduced by Kolmogorov [arXiv:1207.7213] reformulated using Markov chains. Our results generalise all previous partial classifications of finite-valued languages: the classifications of {0, 1}-valued languages on two-element, three-element, and four-element domains obtained by Creignou [JCSS’95], Jonsson et al. [SICOMP’06], and Jonsson et al. [CP’11], respectively; the classification of {0, 1}-valued languages containing all unary functions obtained by Deineko et al. [JACM’06]; the classifi- cations of finite-valued languages on two-element and threeelement domains obtained by Cohen et al. [AIJ’06] and Huber et al. [SODA’13], respectively; the classification of finite- valued languages containing all {0, 1}-valued unary functions obtained by Kolmogorov and Zivn´y [SODA’12]; and ˇthe classification of Min-0-Ext problems obtained recently by Hirai [SODA’13].

Putback-based bidirectional programming allows the programmer to write only one putback transformation, from which the unique corresponding forward transformation is derived for free. The logic of a putback transformation is more sophisticated than that of a forward transformation and does not always give rise to well-behaved bidirectional programs; this calls for more robust language design to support development of well-behaved putback transformations. In this paper, we design and implement a concise core language BiGUL for putback-based bidirectional programming to serve as a foundation for higher-level putback-based languages. BiGUL is completely formally verified in the dependently typed programming language Agda to guarantee that any putback transformation written in BiGUL is well-behaved.

Input-output examples have emerged as a practical and user-friendly specification mechanism for program synthesis in many environments. While example-driven tools have demonstrated tangible impact that has inspired adoption in industry, their underlying semantics are less well-understood: what are "examples" and how do they relate to other kinds of specifications? This paper demonstrates that examples can, in general, be interpreted as refinement types. Seen in this light, program synthesis is the task of finding an inhabitant of such a type. This insight provides an immediate semantic interpretation for examples. Moreover, it enables us to exploit decades of research in type theory as well as its correspondence with intuitionistic logic rather than designing ad hoc theoretical frameworks for synthesis from scratch. We put this observation into practice by formalizing synthesis as proof search in a sequent calculus with intersection and union refinements that we prove to be sound with respect to a conventional type system. In addition, we show how to handle negative examples, which arise from user feedback or counterexample-guided loops. This theory serves as the basis for a prototype implementation that extends our core language to support ML-style algebraic data types and structurally inductive functions. Users can also specify synthesis goals using polymorphic refinements and import monomorphic libraries. The prototype serves as a vehicle for empirically evaluating a number of different strategies for resolving the nondeterminism of the sequent calculus---bottom-up theorem-proving, term enumeration with refinement type checking, and combinations of both---the results of which classify, explain, and validate the design choices of existing synthesis systems. It also provides a platform for measuring the practical value of a specification language that combines "examples" with the more general expressiveness of refinements.

A theory is complete if it does not contain a contradiction, while all of its proper extensions do. In this paper, first we introduce a relative notion of syntactic completeness; then we prove that adding exceptions to a programming language can be done in such a way that the completeness of the language is not made worse. These proofs are formalized in a logical system which is close to the usual syntax for exceptions, and they have been checked with the proof assistant Coq.

In this paper, we study strong normalization of a core language based on System ${\mathsf{F}_\omega}$ which supports programming with finite and infinite structures. Finite data such as finite lists and trees is defined via constructors and manipulated via pattern matching, while infinite data such as streams and infinite trees is defined by observations and synthesized via copattern matching. Taking a type-based approach to strong normalization, we track size information about finite and infinite data in the type. We exploit the duality of pattern and copatterns to give a unifying semantic framework which allows us to elegantly and uniformly support both well-founded induction and coinduction by rewriting. The strong normalization proof is structured around Girard's reducibility candidates. As such, our system allows for non-determinism and does not rely on coverage. Since System ${\mathsf{F}_\omega}$ is general enough that it can be the target of compilation for the Calculus of Constructions, this work is a significant step towards representing observation-based infinite data in proof assistants such as Coq and Agda.

SUMMARY This paper has been motivated by experience gained with specification and code generation of control elements for a software component platform and general-purpose programming language like Java and C. The problem to be addressed is two-fold: first, several domain-specific languages (DSL) are to be employed to express different element concerns (architecture, deployment context, code pattern) and second, porting to another general-purpose language should avoid modification of the specification and related code generation process as much as possible. In both respects, the classical template-based code generation technique proved to be inflexible, requiring the code generator to be blurred with ad hoc encoded DSL facets. The paper addresses the problem by introducing the concept of interoperable DSL family. Each member of the family is built around its core language, which can be further specialized by embedding into a target programming language. Interoperability of these DSLs is achieved at the level of abstract syntax trees (ASTs) with help of queries. As a proof of the concept, we have implemented the queries via the AST transformation rules of the Stratego/XT framework. In the evaluation, we provide a comparison with the original template-based implementation, which clearly indicates the DSL family and AST transformation benefits. We also provide examples of application areas where the concept of interoperable DSL family can be employed (and also indicate how this can be accomplished). Copyright © 2012 John Wiley & Sons, Ltd.

We explore partial type-inference for System F based on type-containment. We consider both cases of a purely functional semantics and a call-by-value stateful semantics. To enable type-inference, we require higher-rank polymorphism to be user-specified via type annotations on source terms. We allow implicit predicative type-containment and explicit impredicative type-instantiation. We obtain a core language that is both as expressive as System F and conservative over ML. Its type system has a simple logical specification and a partial type-reconstruction algorithm that are both very close to the ones for ML. We then propose a surface language where some annotations may be omitted and rebuilt by some algorithmically defined but logically incomplete elaboration mechanism.

In a call-by-value language, representing objects as recursive records requires using an unsafe fixpoint. We design, for a core language including extensible records, a type system which rules out unsafe recursion and still supports the construction of a principal type for each typable term. We illustrate the expressive power of this language with respect to object-oriented programming by introducing a sub-language for “mixin-based” programming.

A Hindley-Milner type system such as ML's seems to prohibit type-indexed values, i.e ., functions that map a family of types to a family of values. Such functions generally perform case analysis on the input types and return values of possibly different types. The goal of our work is to demonstrate how to program with type-indexed values within a Hindley-Milner type system.Our first approach is to interpret an input type as its corresponding value, recursively. This solution is type-safe, in the sense that the ML type system statically prevents any mismatch between the input type and function arguments that depend on this type.Such specific type interpretations, however, prevent us from combining different type-indexed values that share the same type. To meet this objection, we focus on finding a value-independent type encoding that can be shared by different functions. We propose and compare two solutions. One requires first-class and higher-order polymorphism, and, thus, is not implementable in the core language of ML, but it can be programmed using higher-order functors in Standard ML of New Jersey. Its usage, however, is clumsy. The other approach uses embedding/projection functions. It appears to be more practical.We demonstrate the usefulness of type-indexed values through examples including type-directed partial evaluation, C printf-like formatting, and subtype coercions. Finally, we discuss the tradeoffs between our approach and some other solutions based on more expressive typing disciplines.

The importance of reasoning about and refactoring programs is a central tenet of functional programming. Yet our compilers and development toolchains only provide rudimentary support for these tasks. This paper introduces a programmatic and compiler-centric interface that facilitates refactoring and equational reasoning. To develop our ideas, we have implemented HERMIT, a toolkit enabling informal but systematic transformation of Haskell programs from inside the Glasgow Haskell Compiler's optimization pipeline. With HERMIT, users can experiment with optimizations and equational reasoning, while the tedious heavy lifting of performing the actual transformations is done for them. HERMIT provides a transformation API that can be used to build higher-level rewrite tools. One use-case is prototyping new optimizations as clients of this API before being committed to the GHC toolchain. We describe a HERMIT application - a read-eval-print shell for performing transformations using HERMIT. We also demonstrate using this shell to prototype an optimization on a specific example, and report our initial experiences and remaining challenges.

International audience; Recently we showed that an expressive class of mathematical equations can be automatically translated into simulation codes. By focusing on the expressivity of equations formed from continuous functions, this work did not accommodate a wide range of discrete behaviors or a dynamic collection of components. However, the interaction between continuous and hybrid components in many cyber-physical domains is highly coupled, and such systems are often highly dynamic in both respects. This paper gives an overview of a proposed core language for capturing executable hybrid models of highly dynamic cyber-physical systems.

Biomine and ProbLog are two frameworks to implement bisociative information networks (BisoNets). They combine structured data representations with probabilities expressing uncertainty. While Biomine is based on graphs, ProbLog's core language is that of the logic programming language Prolog. This chapter provides an overview of important concepts, terminology, and reasoning tasks addressed in the two systems. It does so in an informal way, focusing on intuition rather than on mathematical definitions. It aims at bridging the gap between network representations and logical ones. ispartof: Bisociative Knowledge Discovery pages:122-143 ispartof: Lecture Notes in Artificial Intelligence vol:7250 pages:122-143 status: published

International audience; Recently we showed that an expressive class of mathematical equations can be automatically translated into simulation codes. Focusing on the expressivity of equations on continuous functions, this work considered only minimal interaction with discrete behaviors and only a static number of statically connected components. However, the interaction between continuous and hybrid components in many cyber physical domains is highly coupled, and such systems are often highly dynamic in both respects. This paper gives an overview of a proposed core language for capturing executable hybrid models of highly dynamic cyber physical systems.

This paper presents ABS, an abstract behavioral specification language for designing executable models of distributed object-oriented systems. The language combines advanced concurrency and synchronization mechanisms for concurrent object groups with a functional language for modeling data. ABS uses asynchronous method calls, interfaces for encapsulation, and cooperative scheduling of method activations inside concurrent objects. This feature combination results in a concurrent object-oriented model which is inherently compositional. We discuss central design issues for ABS and formalize the type system and semantics of Core ABS, a calculus with the main features of ABS. For Core ABS, we prove a subject reduction property which shows that well-typedness is preserved during execution; in particular, "method not understood" errors do not occur at runtime for well-typed ABS models. Finally, we briefly discuss the tool support developed for ABS.

This paper introduces AC, a set of language constructs for composable asynchronous IO in native languages such as C/C++. Unlike traditional synchronous IO interfaces, AC lets a thread issue multiple IO requests so that they can be serviced concurrently, and so that long-latency operations can be overlapped with computation. Unlike traditional asynchronous IO interfaces, AC retains a sequential style of programming without requiring code to use multiple threads, and without requiring code to be "stack-ripped" into chains of callbacks. AC provides an "async" statement to identify opportunities for IO operations to be issued concurrently, a "do..finish" block that waits until any enclosed "async" work is complete, and a "cancel" statement that requests cancellation of unfinished IO within an enclosing "do..finish". We give an operational semantics for a core language. We describe and evaluate implementations that are integrated with message passing on the Barrelfish research OS, and integrated with asynchronous file and network IO on Microsoft Windows. We show that AC offers comparable performance to existing C/C++ interfaces for asynchronous IO, while providing a simpler programming model.

International audience; We offer a solution to the type inference problem for an extension of Hindley and Milner's type system with generalized algebraic data types. Our approach is in two strata. The bottom stratum is a core language that marries type inference in the style of Hindley and Milner with type checking for generalized algebraic data types. This results in an extremely simple specification, where case constructs must carry an explicit type annotation and type conversions must be made explicit. The top stratum consists of (two variants of) an independent shape inference algorithm. This algorithm accepts a source term that contains some explicit type information, propagates this information in a local, predictable way, and produces a new source term that carries more explicit type information. It can be viewed as a preprocessor that helps produce some of the type annotations required by the bottom stratum. It is proven sound in the sense that it never inserts annotations that could contradict the type derivation that the programmer has in mind.

International audience; We show how the full XPath language can be compiled into a minimal subset suited for stream-based evaluation. Specifically, we show how XPath normalization into a core language as proposed in the current W3C Last Call draft of the XPath/XQuery Formal Semantics can be extended such that both the context state and reverse axes can be eliminated from the core XPath (and potentially XQuery) language. This allows execution of (almost) full XPath on any of the emerging streaming subsets.

In a call-by-value language, representing objects as recursive records requires using an unsafe fixpoint. We design, for a core language including extensible records, a type system which rules out unsafe recursion and still supports the reconstruction of a principal type. We illustrate by means of various examples the expressive power of this language with respect to object-oriented programming constructs.

Multimethods offer several well-known advantages over the single dispatching of conventional object-oriented languages, including a simple solution to the "binary method" problem, cleaner implementations of the "visitor," "strategy," and similar design patterns, and a form of "open objects." However, previous work on statically typed multimethods whose arguments are treated symmetrically has required the whole program to be available in order to perform typechecking. We describe Dubious, a simple core language including first-class generic functions with symmetric multimethods, a classless object model, and modules that can be separately typechecked. We identify two sets of restrictions that ensure modular type safety for Dubious as well as an interesting intermediate point between these two. We have proved each of these modular type systems sound.