the proceeding contains 34 papers. the topics discussed include: a type directed translation of MLF to system F;declarative programming for artificial intelligence applications;adding delimited and composable control ...
详细信息
ISBN:
(纸本)9781595938152
the proceeding contains 34 papers. the topics discussed include: a type directed translation of MLF to system F;declarative programming for artificial intelligence applications;adding delimited and composable control to a production programming environment;evaluating high-level distributed language constructs;subtyping and intersection types revisited;user-friendly functionalprogramming for web mashups;a generic usage analysis with subeffect qualifiers;feedback directed implicit parallelism;faster laziness using dynamic pointer tagging;a type system for recursive modules;extensible pattern matching via a lightweight language extension;implicit phasing for R6RS libraries;call-pattern specialisation for haskell programs;bidirectionalization transformation based on automatic derivation of view complement functions;tangible functionalprogramming;and termination analysis and call graph construction for higher-order functional programs.
Over forty years ago, David Barron and Christopher Strachey published a startlingly elegant program for the Cartesian product of a list of lists, expressing it with a three nested occurrences of the function we now ca...
详细信息
FranTk is a new high level library for programming Graphical User Interfaces (GUIs) in Haskell. It is based on Fran (functional Reactive Animation), and uses the notions of Behaviors and Events to structure code. Beha...
详细信息
ISBN:
(纸本)9781581132021
FranTk is a new high level library for programming Graphical User Interfaces (GUIs) in Haskell. It is based on Fran (functional Reactive Animation), and uses the notions of Behaviors and Events to structure code. Behaviors are time-varying, reactive values. they can be used to represent the state of an application. Events are streams of values that occur at discrete points in time. they can be used, for instance, to represent user input. FranTk allows user interfaces to be structured in a more declarative manner than has been possible with previous functional GUI libraries. We demonstrate, through a series of examples, how this is achieved, and why it is important. these examples are elements of a prototype, Air Traffic Control simulator. FranTk uses a binding to the popular Tcl/Tk toolkit to provide a powerful set of platform independent set of widgets. It has been released as a Haskell library that runs under Hugs and GHC.
Adaptive software becomes more and more important as computing is increasingly context-dependent. Runtime adaptability can be achieved by dynamically selecting and applying context-specific code. Role-oriented program...
详细信息
ISBN:
(纸本)9781450369817
Adaptive software becomes more and more important as computing is increasingly context-dependent. Runtime adaptability can be achieved by dynamically selecting and applying context-specific code. Role-oriented programming has been proposed as a paradigm to enable runtime adaptive software by design. Roles change the objects' behavior at runtime and thus allow adapting the software to a given context. However, this increased variability and expressiveness has a direct impact on performance and memory consumption. We found a high overhead in the steady-state performance of executing compositions of adaptations. this paper presents a new approach to use run-time information to construct a dispatch plan that can be executed efficiently by the JVM. the concept of late binding is extended to dynamic function compositions. We evaluated the implementation with a benchmark for role-oriented programming languages leveraging context-dependent role semantics achieving a mean speedup of 2.79x over the regular implementation.
De Bruijn indices are a well known technique for programming with names and binders. they provide a representation that is both simple and canonical. However, programming errors tend to be really easy to make. We prop...
详细信息
ISBN:
(纸本)9781450308656
De Bruijn indices are a well known technique for programming with names and binders. they provide a representation that is both simple and canonical. However, programming errors tend to be really easy to make. We propose a safer programming interface implemented as a library. Whereas indexing the types of names and terms by a numerical bound is a famous technique, we index them by worlds, a different notion of index that is both finer and more abstract. While being more finely typed, our approach incurs no loss of expressiveness or efficiency. Via parametricity we obtain properties about functions polymorphic on worlds. For instance, well-typed world-polymorphic functions over open lambda-terms commute with any renaming of the free variables. Our whole development is conducted within Agda, from the code of the library, to its soundness proof and the properties of external functions. the soundness of our library is demonstrated via the construction of a logical relations argument.
functional logic programming and probabilistic programming have demonstrated the broad benefits of combining laziness (non-strict evaluation with sharing of the results) with non-determinism. Yet these benefits are se...
详细信息
ISBN:
(纸本)9781605583327
functional logic programming and probabilistic programming have demonstrated the broad benefits of combining laziness (non-strict evaluation with sharing of the results) with non-determinism. Yet these benefits are seldom enjoyed in functionalprogramming, because the existing features for non-strictness, sharing, and non-determinism in functional languages are tricky to combine. We present a practical way to write purely functional lazy non-deterministic programs that are efficient and perspicuous. We achieve this goal by embedding the programs into existing languages (such as Haskell, SML, and OCaml) with high-quality implementations, by making choices lazily and representing data with non-deterministic components, by working with custom monadic data types and search strategies, and by providing equational laws for the programmer to reason about their code.
In dependently typed languages run-time values can appear in types, making it possible to give programs more precise types than in languages without dependent types. this can range from keeping track of simple invaria...
详细信息
ISBN:
(纸本)9781450323260
In dependently typed languages run-time values can appear in types, making it possible to give programs more precise types than in languages without dependent types. this can range from keeping track of simple invariants like the length of a list, to full functional correctness. In addition to having some correctness guarantees on the final program, assigning more precise types to programs means that you can get more assistance from the type checker while writing them. this is what I focus on here, demonstrating how the programming environment of AGDA can help you when developing dependently typed programs.
the proceedings contain 12 papers. the topics discussed include: using functional reactive programming for robotic art: an experience report;bridging art and mathematics with Tessella: a scala functional library for r...
ISBN:
(纸本)9798400710995
the proceedings contain 12 papers. the topics discussed include: using functional reactive programming for robotic art: an experience report;bridging art and mathematics with Tessella: a scala functional library for regular polygon finite tessellations of a plane;functional curves and surfaces: algebraic geometry inspired visuals in hydra;Trane: musical Janet on the web;from Konnakol to live coding;the Maquette Monad;diffusion-based sound synthesis in music production;a progressive-adaptive music generator (PAMG): an approach to interactive procedural music for videogames;and demo: progressive-adaptive music generator (PAMG) and the trial game.
We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating sy...
详细信息
ISBN:
(纸本)9781450323260
We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally the saying that C is a "macro assembly language": we introduce an expressive notion of certified low-level macros, sufficient to build up the usual features of C and beyond as macros with no special support in the core. Furthermore, our macros have integrated support for strongest postcondition calculation and verification condition generation, so that we can provide a high-productivity formal verification environment within Coq for programs composed from any combination of macros. Our macro interface is expressive enough to support features that low-level programs usually only access through external tools with no formal guarantees, such as declarative parsing or SQL-inspired querying. the abstraction level of these macros only imposes a compile-time cost, via the execution of functional Coq programs that compute programs in our intermediate language;but the run-time cost is not substantially greater than for more conventional C code. We describe our experiences constructing a full C-like language stack using macros, with some experiments on the verifiability and performance of individual programs running on that stack.
We give a denotational model for graphical user interface (GUI) programming using the Cartesian closed category of ultrametric spaces. the ultrametric structure enforces causality restrictions on reactive systems and ...
详细信息
ISBN:
(纸本)9781450308656
We give a denotational model for graphical user interface (GUI) programming using the Cartesian closed category of ultrametric spaces. the ultrametric structure enforces causality restrictions on reactive systems and allows well-founded recursive definitions by a generalization of guardedness. We capture the arbitrariness of user input (e. g., a user gets to decide the stream of clicks she sends to a program) by making use of the fact that the closed subsets of an ultrametric space themselves form an ultrametric space, allowing us to interpret nondeterminism with a "powerspace" monad. Algebras for the powerspace monad yield a model of intuitionistic linear logic, which we exploit in the definition of a mixed linear/non-linear domain-specific language for writing GUI programs. the non-linear part of the language is used for writing reactive stream-processing functions whilst the linear sublanguage naturally captures the generativity and usage constraints on the various linear objects in GUIs, such as the elements of a DOM or scene graph. We have implemented this DSL as an extension to OCaml, and give examples demonstrating that programs in this style can be short and readable.
暂无评论