Workshop WGP 2015 – Author Index |
Contents -
Abstracts -
Authors
|
Arni, Julian K. |
![]() Alp Mestanogullari, Sönke Hahn, Julian K. Arni, and Andres Löh (Kitty Knows, UK; Zalora SEA, Singapore; Well-Typed, UK) We describe the design and motivation for Servant, an extensible, type-level DSL for describing Web APIs. Servant APIs are Haskell types. An API type can be interpreted in several different ways: as a server that processes requests, interprets them and dispatches them to appropriate handlers; as a client that can correctly query the endpoints of the API; as systematic documentation for the API; and more. Servant is fully extensible: the API language can be augmented with new constructs, and new interpretations can be defined. The key Haskell features making all this possible are data kinds, (open) type families and (open) type classes. The techniques we use are reminiscent of general-purpose generic programming. However, where most generic programming libraries are interested in automatically deriving programs for a large class of datatypes from many different domains, we are only interested in a small class of datatypes that is used in the DSL for describing APIs. ![]() |
|
Firsov, Denis |
![]() Denis Firsov and Tarmo Uustalu (Tallinn University of Technology, Estonia) Definitions of many mathematical structures used in computer science are parametrized by finite sets. To work with such structures in proof assistants, we need to be able to explain what a finite set is. In constructive mathematics, a widely used definition is listability: a set is considered to be finite, if its elements can be listed completely. In this paper, we formalize different variations of this definition in the Agda programming language. We develop a toolbox for boilerplate-free programming with finite sets that arise as subsets of some base set with decidable equality. Among other things we implement combinators for defining functions from finite sets and a prover for quantified formulas over decidable properties on finite sets. ![]() |
|
Hahn, Sönke |
![]() Alp Mestanogullari, Sönke Hahn, Julian K. Arni, and Andres Löh (Kitty Knows, UK; Zalora SEA, Singapore; Well-Typed, UK) We describe the design and motivation for Servant, an extensible, type-level DSL for describing Web APIs. Servant APIs are Haskell types. An API type can be interpreted in several different ways: as a server that processes requests, interprets them and dispatches them to appropriate handlers; as a client that can correctly query the endpoints of the API; as systematic documentation for the API; and more. Servant is fully extensible: the API language can be augmented with new constructs, and new interpretations can be defined. The key Haskell features making all this possible are data kinds, (open) type families and (open) type classes. The techniques we use are reminiscent of general-purpose generic programming. However, where most generic programming libraries are interested in automatically deriving programs for a large class of datatypes from many different domains, we are only interested in a small class of datatypes that is used in the DSL for describing APIs. ![]() |
|
Jespersen, Thomas Bracht Laumann |
![]() Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen (University of Copenhagen, Denmark) We present a library for specifying session types implemented in Rust, and discuss practical use cases through examples and demonstrate how session types may be used in a large-scale application. Specifically we adapt parts of the ad-hoc communication patterns in the Servo browser engine to use session typed channels. Session types provide a protocol abstraction, expanding on traditional typed communication channels, to ensure that communication takes place according to a specified protocol. Thus, the library allows us to provide compile-time guarantees of adherence to a specific protocol without incurring significant run-time penalties. ![]() |
|
Larsen, Ken Friis |
![]() Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen (University of Copenhagen, Denmark) We present a library for specifying session types implemented in Rust, and discuss practical use cases through examples and demonstrate how session types may be used in a large-scale application. Specifically we adapt parts of the ad-hoc communication patterns in the Servo browser engine to use session typed channels. Session types provide a protocol abstraction, expanding on traditional typed communication channels, to ensure that communication takes place according to a specified protocol. Thus, the library allows us to provide compile-time guarantees of adherence to a specific protocol without incurring significant run-time penalties. ![]() |
|
Löh, Andres |
![]() Alp Mestanogullari, Sönke Hahn, Julian K. Arni, and Andres Löh (Kitty Knows, UK; Zalora SEA, Singapore; Well-Typed, UK) We describe the design and motivation for Servant, an extensible, type-level DSL for describing Web APIs. Servant APIs are Haskell types. An API type can be interpreted in several different ways: as a server that processes requests, interprets them and dispatches them to appropriate handlers; as a client that can correctly query the endpoints of the API; as systematic documentation for the API; and more. Servant is fully extensible: the API language can be augmented with new constructs, and new interpretations can be defined. The key Haskell features making all this possible are data kinds, (open) type families and (open) type classes. The techniques we use are reminiscent of general-purpose generic programming. However, where most generic programming libraries are interested in automatically deriving programs for a large class of datatypes from many different domains, we are only interested in a small class of datatypes that is used in the DSL for describing APIs. ![]() |
|
Mestanogullari, Alp |
![]() Alp Mestanogullari, Sönke Hahn, Julian K. Arni, and Andres Löh (Kitty Knows, UK; Zalora SEA, Singapore; Well-Typed, UK) We describe the design and motivation for Servant, an extensible, type-level DSL for describing Web APIs. Servant APIs are Haskell types. An API type can be interpreted in several different ways: as a server that processes requests, interprets them and dispatches them to appropriate handlers; as a client that can correctly query the endpoints of the API; as systematic documentation for the API; and more. Servant is fully extensible: the API language can be augmented with new constructs, and new interpretations can be defined. The key Haskell features making all this possible are data kinds, (open) type families and (open) type classes. The techniques we use are reminiscent of general-purpose generic programming. However, where most generic programming libraries are interested in automatically deriving programs for a large class of datatypes from many different domains, we are only interested in a small class of datatypes that is used in the DSL for describing APIs. ![]() |
|
Munksgaard, Philip |
![]() Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen (University of Copenhagen, Denmark) We present a library for specifying session types implemented in Rust, and discuss practical use cases through examples and demonstrate how session types may be used in a large-scale application. Specifically we adapt parts of the ad-hoc communication patterns in the Servo browser engine to use session typed channels. Session types provide a protocol abstraction, expanding on traditional typed communication channels, to ensure that communication takes place according to a specified protocol. Thus, the library allows us to provide compile-time guarantees of adherence to a specific protocol without incurring significant run-time penalties. ![]() |
|
Rodriguez, Ernesto |
![]() Ernesto Rodriguez and Wouter Swierstra (Utrecht University, Netherlands) Datatype generic programming enables programmers to define functions by induction over the structure of types on which these functions operate. This paper presents a library for datatype generic programming in F#, built on top of the .NET reflection mechanism.The generic functions defined using this library can be called by any other language running on the .NET platform. ![]() |
|
Swierstra, Wouter |
![]() Ernesto Rodriguez and Wouter Swierstra (Utrecht University, Netherlands) Datatype generic programming enables programmers to define functions by induction over the structure of types on which these functions operate. This paper presents a library for datatype generic programming in F#, built on top of the .NET reflection mechanism.The generic functions defined using this library can be called by any other language running on the .NET platform. ![]() |
|
Uustalu, Tarmo |
![]() Denis Firsov and Tarmo Uustalu (Tallinn University of Technology, Estonia) Definitions of many mathematical structures used in computer science are parametrized by finite sets. To work with such structures in proof assistants, we need to be able to explain what a finite set is. In constructive mathematics, a widely used definition is listability: a set is considered to be finite, if its elements can be listed completely. In this paper, we formalize different variations of this definition in the Agda programming language. We develop a toolbox for boilerplate-free programming with finite sets that arise as subsets of some base set with decidable equality. Among other things we implement combinators for defining functions from finite sets and a prover for quantified formulas over decidable properties on finite sets. ![]() |
11 authors
proc time: 0.83