Workshop WGP 2015 – Author Index |
Contents -
Abstracts -
Authors
|
| Arni, Julian K. |
WGP '15: "Type-Level Web APIs with Servant: ..."
Type-Level Web APIs with Servant: An Exercise in Domain-Specific Generic Programming
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. 
@InProceedings{WGP15p1,
author = {Alp Mestanogullari and Sönke Hahn and Julian K. Arni and Andres Löh},
title = {Type-Level Web APIs with Servant: An Exercise in Domain-Specific Generic Programming},
booktitle = {Proc.\ WGP},
publisher = {ACM},
pages = {1--12},
doi = {},
year = {2015},
}
|
|
| Firsov, Denis |
WGP '15: "Dependently Typed Programming ..."
Dependently Typed Programming with Finite Sets
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.
@InProceedings{WGP15p33,
author = {Denis Firsov and Tarmo Uustalu},
title = {Dependently Typed Programming with Finite Sets},
booktitle = {Proc.\ WGP},
publisher = {ACM},
pages = {33--44},
doi = {},
year = {2015},
}
|
|
| Hahn, Sönke |
WGP '15: "Type-Level Web APIs with Servant: ..."
Type-Level Web APIs with Servant: An Exercise in Domain-Specific Generic Programming
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.
@InProceedings{WGP15p1,
author = {Alp Mestanogullari and Sönke Hahn and Julian K. Arni and Andres Löh},
title = {Type-Level Web APIs with Servant: An Exercise in Domain-Specific Generic Programming},
booktitle = {Proc.\ WGP},
publisher = {ACM},
pages = {1--12},
doi = {},
year = {2015},
}
|
|
| Jespersen, Thomas Bracht Laumann |
WGP '15: "Session Types for Rust ..."
Session Types for Rust
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.
@InProceedings{WGP15p13,
author = {Thomas Bracht Laumann Jespersen and Philip Munksgaard and Ken Friis Larsen},
title = {Session Types for Rust},
booktitle = {Proc.\ WGP},
publisher = {ACM},
pages = {13--22},
doi = {},
year = {2015},
}
|
|
| Larsen, Ken Friis |
WGP '15: "Session Types for Rust ..."
Session Types for Rust
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.
@InProceedings{WGP15p13,
author = {Thomas Bracht Laumann Jespersen and Philip Munksgaard and Ken Friis Larsen},
title = {Session Types for Rust},
booktitle = {Proc.\ WGP},
publisher = {ACM},
pages = {13--22},
doi = {},
year = {2015},
}
|
|
| Löh, Andres |
WGP '15: "Type-Level Web APIs with Servant: ..."
Type-Level Web APIs with Servant: An Exercise in Domain-Specific Generic Programming
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.
@InProceedings{WGP15p1,
author = {Alp Mestanogullari and Sönke Hahn and Julian K. Arni and Andres Löh},
title = {Type-Level Web APIs with Servant: An Exercise in Domain-Specific Generic Programming},
booktitle = {Proc.\ WGP},
publisher = {ACM},
pages = {1--12},
doi = {},
year = {2015},
}
|
|
| Mestanogullari, Alp |
WGP '15: "Type-Level Web APIs with Servant: ..."
Type-Level Web APIs with Servant: An Exercise in Domain-Specific Generic Programming
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.
@InProceedings{WGP15p1,
author = {Alp Mestanogullari and Sönke Hahn and Julian K. Arni and Andres Löh},
title = {Type-Level Web APIs with Servant: An Exercise in Domain-Specific Generic Programming},
booktitle = {Proc.\ WGP},
publisher = {ACM},
pages = {1--12},
doi = {},
year = {2015},
}
|
|
| Munksgaard, Philip |
WGP '15: "Session Types for Rust ..."
Session Types for Rust
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.
@InProceedings{WGP15p13,
author = {Thomas Bracht Laumann Jespersen and Philip Munksgaard and Ken Friis Larsen},
title = {Session Types for Rust},
booktitle = {Proc.\ WGP},
publisher = {ACM},
pages = {13--22},
doi = {},
year = {2015},
}
|
|
| Rodriguez, Ernesto |
WGP '15: "Datatype Generic Programming ..."
Datatype Generic Programming in F#
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.
@InProceedings{WGP15p23,
author = {Ernesto Rodriguez and Wouter Swierstra},
title = {Datatype Generic Programming in F#},
booktitle = {Proc.\ WGP},
publisher = {ACM},
pages = {23--32},
doi = {},
year = {2015},
}
|
|
 |
Swierstra, Wouter |
WGP '15: "Datatype Generic Programming ..."
Datatype Generic Programming in F#
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.
@InProceedings{WGP15p23,
author = {Ernesto Rodriguez and Wouter Swierstra},
title = {Datatype Generic Programming in F#},
booktitle = {Proc.\ WGP},
publisher = {ACM},
pages = {23--32},
doi = {},
year = {2015},
}
|
| Uustalu, Tarmo |
WGP '15: "Dependently Typed Programming ..."
Dependently Typed Programming with Finite Sets
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.
@InProceedings{WGP15p33,
author = {Denis Firsov and Tarmo Uustalu},
title = {Dependently Typed Programming with Finite Sets},
booktitle = {Proc.\ WGP},
publisher = {ACM},
pages = {33--44},
doi = {},
year = {2015},
}
|
11 authors
proc time: 1.05