Sciweavers

FLOPS
2010
Springer
13 years 10 months ago
A Skeleton for Distributed Work Pools in Eden
We present a flexible skeleton for implementing distributed work pools in our parallel functional language Eden. The skeleton manages a pool of tasks (work pool) in a distributed ...
Mischa Dieterle, Jost Berthold, Rita Loogen
FLOPS
2010
Springer
13 years 10 months ago
Proving Injectivity of Functions via Program Inversion in Term Rewriting
Injectivity is one of the important properties for functions while it is undecidable in general and decidable for linear treeless functions. In this paper, we show new sufficient c...
Naoki Nishida, Masahiko Sakai
FLOPS
2010
Springer
14 years 4 months ago
Tag-Free Combinators for Binding-Time Polymorphic Program Generation
Abstract. Binding-time polymorphism enables a highly flexible bindingtime analysis for offline partial evaluation. This work provides the tools to translate this flexibility into...
Peter Thiemann, Martin Sulzmann
FLOPS
2010
Springer
14 years 6 months ago
Haskell Type Constraints Unleashed
Dominic A. Orchard, Tom Schrijvers
FLOPS
2010
Springer
14 years 6 months ago
Code Generation via Higher-Order Rewrite Systems
Abstract. We present the meta-theory behind the code generation facilities of Isabelle/HOL. To bridge the gap between the source (higherorder logic with type classes) and the many ...
Florian Haftmann, Tobias Nipkow
FLOPS
2010
Springer
14 years 6 months ago
PiSigma: Dependent Types without the Sugar
Thorsten Altenkirch, Nils Anders Danielsson, Andre...
FLOPS
2010
Springer
14 years 6 months ago
A Church-Style Intermediate Language for MLF
MLF is a type system that seamlessly merges ML-style implicit but second-class polymorphism with System F explicit first-class polymorphism. We present xMLF, a Church-style versi...
Didier Rémy, Boris Yakobowski
FLOPS
2010
Springer
14 years 6 months ago
Automatically Generating Counterexamples to Naive Free Theorems
Disproof can be as important as proof in studying programs and programming languages. In particular, side conditions in a statement about program behavior are sometimes best unders...
Daniel Seidel, Janis Voigtländer
FLOPS
2010
Springer
14 years 6 months ago
Beluga: Programming with Dependent Types, Contextual Data, and Contexts
The logical framework LF provides an elegant foundation for specifying formal systems and proofs and it is used successfully in a wide range of applications such as certifying code...
Brigitte Pientka
FLOPS
2010
Springer
14 years 6 months ago
Complexity Analysis by Graph Rewriting
Recently, many techniques have been introduced that allow the (automated) classification of the runtime complexity of term rewrite systems (TRSs for short). In this paper we show ...
Martin Avanzini, Georg Moser