1,721,030 research outputs found
IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages
Full text linkImplementation and Application of Functional Languages: 19th International Workshop, IFL 2007, Freiburg, Germany, September 27-29, 2007. Revised Selected Papers
No full textThis book constitutes the thoroughly refereed post-proceedings of the 19th International Workshop on Implementation and Applications of Functional Languages, IFL 2007, held in Freiburg, Germany in September 2007.
The 15 revised full papers presented went through two rounds of reviewing and improvement and were selected from 33 submissions. The papers address all current theoretical and methodological issues on functional and function-based languages such as type checking, contract checking, compilation, parallelism, development and debugging, data structures, parsing as well as various performance related concepts
PPDP '14: Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming
No full textLinear, bounded, functional pretty-printing
Full text linkWe present two implementations of Oppen's pretty-printing algorithm in Haskell that meet the efficiency of Oppen's imperative solution but have a simpler, clear structure. We start with an implementation that uses lazy evaluation to simulate two co-operating processes. Then we present an implementation that uses higher-order functions for delimited continuations to simulate co-routines with explicit scheduling
Transparent Ajax and Client-Site Evaluation of iTasks
Full text linkContains fulltext :
36638.pdf (Publisher’s version ) (Open Access)IFL 200
Implementation and Application of Functional Languages: 20th International Symposium, IFL 2008; Hatfield, UK, September 2008; Revised Selected Papers
Full text linkS-Net is a declarative coordination language and component technology aimed at modern multi-core/many-core architectures and systems-on-chip. It builds on the concept of stream processing to structure networks of communicating asynchronous components, which can be implemented using a conventional (sequential) language. In this paper we present the architecture of our S-Net implementation. After sketching out the interplay between compiler and runtime system, we characterise the deployment and operational behaviour of our multithreaded runtime system for contemporary multi-core processors. Preliminary runtime figures demonstrate the effectiveness of our approach. <br/
Algorithmic debugging for complex lazy functional programs
Full text linkAn algorithmic debugger finds defects in programs by systematic search. It relies on the programmer to direct the search by answering a series of yes/no questions about the correctness of specific function applications and their results. Existing algorithmic debuggers for a lazy functional language work well for small simple programs but cannot be used to locate defects in complex programs for two reasons: Firstly, to collect the information required for algorithmic debugging existing debuggers use different but complex implementations. Therefore, these debuggers are hard to maintain and do not support all the latest language features. As a consequence, programs with unsupported language features cannot be debugged. Also inclusion of a library using unsupported languages features can make algorithmic debugging unusable even when the programmer is not interested in debugging the library. Secondly, algorithmic debugging breaks down when the size or number of questions is too great for the programmer to handle. This is a pity, because, even though algorithmic debugging is a promising method for locating defects, many real-world programs are too complex for the method to be usuable. I claim that the techniques in in this thesis make algorithmic debugging useable for a much more complex lazy functional programs. I present a novel method for collecting the information required for algorithmically debugging a lazy functional program. The method is non-invasive, uses program annotations in suspected modules only and has a simple implementation. My method supports all of Haskell, including laziness, higher-order functions and exceptions. Future language extensions can be supported without changes, or with minimal changes, to the implementation of the debugger. With my method the programmer can focus on untrusted code -- lots of trusted libraries are unaffected. This makes traces, and hence the amount of questions that needs to be answered, more manageable. I give a type-generic definition to support custom types defined by the programmer. Furthermore, I propose a method that re-uses properties to answer automatically some of the questions arising during algorithmic debugging, and to replace others by simpler questions. Properties may already be present in the code for testing; the programmer can also encode a specification or reference implementation as a property, or add a new property in response to a statement they are asked to judge
Verified compilation of a purely functional language to a realistic machine semantics
Full text linkFormal verification of a compiler offers the ultimate understanding of the behaviour of compiled code: a mathematical proof relates the semantics of each output program to that of its corresponding input. Users can rely on the same formally-specified understanding of source-level behaviour as the compiler, so any reasoning about source code applies equally to the machine code which is actually executed. Critically, these guarantees demand faith only in a minimal trusted computing base (TCB). To date, only two general-purpose, end-to-end verified compilers exist: CompCert and CakeML, which compile a C-like and an ML-like language respectively.
In this dissertation, I advance the state of the art in general-purpose, end-to-end compiler verification in two ways. First, I present PureCake, the first such verified compiler for a purely functional, Haskell-like language. Second, I derive the first compiler correctness theorem backed by a realistic machine semantics, that is, an official specification for the Armv8 instruction set architecture.
Both advancements build on CakeML. PureCake extends CakeML's guarantees outwards, using it as an unmodified building block to demonstrate that we can reuse verified compilers as we do unverified ones. The key difference is that reuse of a verified compiler must consider not only its external implementation interface, but also its proof interface: its top-level theorems and TCB. Conversely, a realistic machine semantics for Armv8 strengthens the root of CakeML's trust, reducing its TCB. Now, both CakeML and the hardware it targets share a common understanding of Armv8 behaviour which is derived from the same official sources.
Composing these two advancements fulfils the title of this dissertation: PureCake has an end-to-end correctness theorem which spans from a purely functional, Haskell-like language to a realistic, official machine semantics
Debugging Type Errors with a Blackbox Compiler
Full text linkType error debugging can be a laborious yet necessary process for programmers of statically typed functional programming languages. Often a compiler compounds this by inaccurately reporting the location of a type error, a problem that has been a subject of research for over thirty years. However, despite its long history, the solutions proposed are often reliant on direct modifications to the compiler, often distributed in the form of patches. These patches append another level of arduous activity to the task of debugging, keeping them modernised to the ever-changing programming language they support.
This thesis investigates an additional option; the blackbox compiler. Split into three central parts, it shows the individual solutions involved in using a blackbox compiler to debug type errors in functional programming languages. First is a demonstration of how the combination of a blackbox compiler and a generic debugging algorithm can successfully locate type errors. Next tackled is a side-effect of this new combination, the introduction of extra errors, combated with a new speed boosted algorithm, evaluated with a proposed framework based on Data Science techniques to quantify the quality of a type error debugger. Lastly, the algorithms employed throughout this thesis, along with the blackbox compiler, have agnostic properties, they do not need language-specific knowledge. Thus, the final part presents utilising the agnostic abilities for an agnostic debugger to locate type errors
On the Validation of Specifications used in Model-Based Testing
Full text linkContains fulltext :
35294.pdf (Publisher’s version ) (Open Access)IFL 200
- …
