| 1. |
- Bernardy, Jean-Philippe, 1978
(författare)
-
Yi An Editor in Haskell for Haskell
- 2009
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - 0730-8566. ; 44:2, s. 61-62
-
Tidskriftsartikel (refereegranskat)abstract
- Yi is a text editor written in Haskell and extensible in Haskell. We take advantage of Haskell's expressive power to define embedded DSLs that form the foundation of the editor. In turn, these DSLs provide a flexible mechanism to create extended versions
|
|
| 2. |
- Danielsson, Nils Anders, 1979
(författare)
-
Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures
- 2008
-
Ingår i: 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'08; San Francisco, CA; United States; 7 January 2008 through 12 January 2008. - New York, NY, USA : ACM. - 0730-8566. - 9781595936899 ; , s. 133-144
-
Konferensbidrag (refereegranskat)abstract
- Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis is frequently subtle, requiring careful attention to detail, and hence formalising it is valuable. This paper describes a simple library which can be used to make the analysis of a class of purely functional data structures and algorithms almost fully formal. The basic idea is to use the type system to annotate every function with the time required to compute its result. An annotated monad is used to combine time complexity annotations. The library has been used to analyse some existing data structures, for instance the deque operations of Hinze and Paterson's finger trees.
|
|
| 3. |
- Hughes, John, 1958
(författare)
-
Experiences from teaching functional programming at Chalmers
- 2008
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - : Association for Computing Machinery (ACM). - 0730-8566 .- 0362-1340 .- 1558-1160. ; 43:11, s. 77-80
-
Tidskriftsartikel (refereegranskat)abstract
- John Hughes shared his experiences of teaching functional programming at Chalmers University in Gothenburg along with the successes and the problems he faced. His highest priority was to convince students that they could write real, interesting programs in Haskell by the end of the first course. He eliminated all the course material directly irrelevant to programming like a section on program proofs. He used to taught the material in a different order to most functional programming texts, like introducing Haskell input/output in the first lecture. He also included two lectures on GUI programming (using wxHaskell), building a simple straight-line-diagram editor in a couple of pages of code. He also introduced QuickCheck (random property-based) testing as part of the course, teaching students first to write the left-hand-side and type of a function, then its property, and finally its right-hand-side.
|
|
| 4. |
- Lindblad, Fredrik, 1973, et al.
(författare)
-
SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values
- 2008
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - 0730-8566. ; 44:2, s. 37-48
-
Tidskriftsartikel (refereegranskat)abstract
- This paper describes two Haskell libraries for property-based testing. Following the lead of QuickCheck, these testing libraries SmallCheck and Lazy SmallCheck also use type-based generators to obtain test-sets of finite values for which properties are checked, and report any counter-examples found. But instead of using a sample of randomly generated values they test properties for all values up to some limiting depth, progressively increasing this limit. The paper explains the design and implementation of both libraries and evaluates them in comparison with each other and with QuickCheck.
|
|
| 5. |
- Oliveira, Bruno C D S, et al.
(författare)
-
The visitor pattern as a reusable, generic, type-safe component
- 2008
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - 0730-8566. ; 43:10, s. 439-456
-
Tidskriftsartikel (refereegranskat)abstract
- The VISITOR design pattern shows how to separate the structure of an object hierarchy from the behaviour of traversals over that hierarchy. The pattern is very flexible; this very flexibility makes it difficult to capture the pattern as anything more formal than prose, pictures and prototypes.We show how to capture the essence of the VISITOR pattern as a reusable software library, by using advanced type system features appearing in modern object-oriented languages such as Scala. We preserve type-safety statically and modularly: no reflection or similar mechanisms are used and modules can be independently compiled. The library is generic, in two senses: not only is it parametrised by both the return type and the shape of the object hierarchy, but also it allows a number of implementation choices (internal versus external control, imperative versus functional behaviour, orthogonal aspects such as tracing and memoisation) to be specified by parameters rather than fixed in early design decisions. Finally, we propose a generalised datatype-like notation,on top of our visitor library: this provides a convenient functional decomposition style in object-oriented languages.
|
|
| 6. |
- Russo, Alejandro, 1978, et al.
(författare)
-
A Library for Light-Weight Information-Flow Security in Haskell
- 2009
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - 0730-8566. ; 44:2, s. 13-24
-
Tidskriftsartikel (refereegranskat)abstract
- Protecting confidentiality of data has become increasingly important for computing systems. Information-flow techniques have been developed over the years to achieve that purpose, leading to special-purpose languages that guarantee information-flow security in programs. However, rather than producing a new language from scratch, information-flow security can also be provided as a library. This has been done previously in Haskell using the arrow framework. In this paper, we show that arrows are not necessary to design such libraries and that a less general notion, namely monads, is sufficient to achieve the same goals. We present a monadic library to provide information-flow security for Haskell programs. The library introduces mechanisms to protect confidentiality of data for pure computations, that we then easily, and modularly, extend to include dealing with side-effects. We also present combinators to dynamically enforce different declassification policies when release of information is required in a controlled manner. It is possible to enforce policies related to what, by whom, and when information is released or a combination of them. The well-known concept of monads together with the light-weight characteristic of our approach makes the library suitable to build applications where confidentiality of data is an issue.
|
|
| 7. |
- Viera, M., et al.
(författare)
-
Attribute Grammars Fly First-Class How to do Aspect Oriented Programming in Haskell
- 2009
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - New York, NY, USA : ACM. - 0730-8566. - 9781605583327 ; 44:9, s. 245-256
-
Tidskriftsartikel (refereegranskat)abstract
- Attribute Grammars (AGs), a general-purpose formalism for describing recursive computations over data types, avoid the trade-off which arises when building software incrementally: should it be easy to add new data types and data type alternatives or to add new operations on existing data types? However, AGs are usually implemented as a pre-processor, leaving e. g. type checking to later processing phases and making interactive development, proper error reporting and debugging difficult. Embedding AG into Haskell as a combinator library solves these problems. Previous attempts at embedding AGs as a domain-specific language were based on extensible records and thus exploiting Haskell's type system to check the well-formedness of the AG, but fell short in compactness and the possibility to abstract over oft occurring AG patterns. Other attempts used a very generic mapping for which the AG well-formedness could not be statically checked. We present a typed embedding of AG in Haskell satisfying all these requirements. The key lies in using HList-like typed heterogeneous collections (extensible polymorphic records) and expressing AG well-formedness conditions as type-level predicates (i.e., type-class constraints). By further type-level programming we can also express common programming patterns, corresponding to the typical use cases of monads such as Reader, Writer and State. The paper presents a realistic example of type-class-based type-level programming in Haskell.
|
|
| 8. |
- Xu, D. N., et al.
(författare)
-
Static contract checking for haskell
- 2009
-
Ingår i: Conference Record of the Annual ACM Symposium on Principles of Programming Languages. - New York, NY, USA : ACM. - 0730-8566. - 9781605583792 ; , s. 41-52
-
Konferensbidrag (refereegranskat)abstract
- Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and for systems that are guarded by runtime checks. Static verification techniques have been applied to imperative and object-oriented languages, like Java and C#, but few have been applied to a higher-order lazy functional language, like Haskell. In this paper, we describe a sound and automatic static verification framework for Haskell, that is based on contracts and symbolic execution. Our approach is modular and gives precise blame assignments at compile-time in the presence of higher-order functions and laziness.
|
|
| 9. |
- Xu, D. N., et al.
(författare)
-
Static Contract Checking for Haskell
- 2009
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - : Association for Computing Machinery (ACM). - 0730-8566 .- 0362-1340 .- 1558-1160. ; 44:1, s. 41-52
-
Tidskriftsartikel (refereegranskat)abstract
- Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and for systems that are guarded by runtime checks. Static verification techniques have been applied to imperative and object-oriented languages, like Java and C#, but few have been applied to a higher-order lazy functional language, like Haskell. In this paper, we describe a sound and automatic static verification framework for Haskell, that is based on contracts and symbolic execution. Our approach is modular and gives precise blame assignments at compile-time in the presence of higher-order functions and laziness.
|
|
