Export Citations
Save this search
Please login to be able to save your searches and receive alerts for new content matching your search criteria.
- research-articleAugust 2022
A completely unique account of enumeration
Proceedings of the ACM on Programming Languages (PACMPL), Volume 6, Issue ICFPArticle No.: 105, Pages 411–437https://doi.org/10.1145/3547636How can we enumerate the inhabitants of an algebraic datatype? This paper explores a datatype generic solution that works for all regular types and indexed families. The enumerators presented here are provably both complete and unique—they will ...
Datatype-generic programming meets elaborator reflection
Proceedings of the ACM on Programming Languages (PACMPL), Volume 6, Issue ICFPArticle No.: 98, Pages 225–253https://doi.org/10.1145/3547629Datatype-generic programming is natural and useful in dependently typed languages such as Agda. However, datatype-generic libraries in Agda are not reused as much as they should be, because traditionally they work only on datatypes decoded from a library’...
- research-articleSeptember 2018
Declarative GUIs: Simple, Consistent, and Verified
PPDP '18: Proceedings of the 20th International Symposium on Principles and Practice of Declarative ProgrammingArticle No.: 4, Pages 1–15https://doi.org/10.1145/3236950.3236962Graphical user interfaces (GUIs) are ubiquitous in real-world software and a notorious source of bugs that are difficult to catch through software testing. Model checking has been used to prove the absence of certain kinds of bugs, but model checking ...
- research-articleAugust 2015
Dependently typed programming with finite sets
WGP 2015: Proceedings of the 11th ACM SIGPLAN Workshop on Generic ProgrammingPages 33–44https://doi.org/10.1145/2808098.2808102Definitions 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 ...
- research-articleJanuary 2015
Certified Normalization of Context-Free Grammars
CPP '15: Proceedings of the 2015 Conference on Certified Programs and ProofsPages 167–174https://doi.org/10.1145/2676724.2693177Every context-free grammar can be transformed into an equivalent one in the Chomsky normal form by a sequence of four transformations. In this work on formalization of language theory, we prove formally in the Agda dependently typed programming language ...
- research-articleSeptember 2013
Relational algebraic ornaments
DTP '13: Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programmingPages 37–48https://doi.org/10.1145/2502409.2502413Dependently typed programming is hard, because ideally dependently typed programs should share structure with their correctness proofs, but there are very few guidelines on how one can arrive at such integrated programs. McBride's algebraic ...
- research-articleSeptember 2012
Dependently typed programming with singletons
Haskell '12: Proceedings of the 2012 Haskell SymposiumPages 117–130https://doi.org/10.1145/2364506.2364522Haskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas ...
Also Published in:
ACM SIGPLAN Notices: Volume 47 Issue 12 - research-articleSeptember 2011
Modularising inductive families
WGP '11: Proceedings of the seventh ACM SIGPLAN workshop on Generic programmingPages 13–24https://doi.org/10.1145/2036918.2036921Dependently typed programmers are encouraged to use inductive families to integrate constraints with data construction. Different constraints are used in different contexts, leading to different versions of datatypes for the same data structure. Modular ...
- ArticleMay 2011
Dependently-typed formalisation of relation-algebraic abstractions
RAMICS'11: Proceedings of the 12th international conference on Relational and algebraic methods in computer sciencePages 230–247We present a formalisation in the dependently-typed programming language Agda2 of basic category and allegory theory, and of generalised algebras where function symbols are interpreted in a parameter category. We use this nestable algebra construction ...
- research-articleNovember 2010
Language-based verification will change the world
FoSER '10: Proceedings of the FSE/SDP workshop on Future of software engineering researchPages 343–348https://doi.org/10.1145/1882362.1882432We argue that lightweight, language-based verification is poised to enter mainstream industrial use, where it will have a major impact on software quality and reliability. We explain how language-based approaches based on so-called dependent types are ...
- ArticleJune 2010
Dependently typed grammars
MPC'10: Proceedings of the 10th international conference on Mathematics of program constructionPages 58–79Parser combinators are a popular tool for designing parsers in functional programming languages. If such combinators generate an abstract representation of the grammar as an intermediate step, it becomes easier to perform analyses and transformations ...
- research-articleJanuary 2010
Resource typing in Guru
PLPV '10: Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verificationPages 27–38https://doi.org/10.1145/1707790.1707796This paper presents a resource typing framework for the Guru verified-programming language, in which abstractions for various kinds of program resources can be defined. Implemented examples include reference-counted data, mutable arrays, and heap-...
- research-articleJanuary 2009
Verified programming in Guru
PLPV '09: Proceedings of the 3rd workshop on Programming languages meets program verificationPages 49–58https://doi.org/10.1145/1481848.1481856Operational Type Theory (OpTT) is a type theory allowing possibly diverging programs while retaining decidability of type checking and a consistent logic. This is done by distinguishing proofs and (program) terms, as well as formulas and types. The ...
- ArticleJanuary 2007
Constructing strictly positive families
CATS '07: Proceedings of the thirteenth Australasian symposium on Theory of computing - Volume 65Pages 111–121In order to represent, compute and reason with advanced data types one must go beyond the traditional treatment of data types as being inductive types and, instead, consider them as inductive families. Strictly positive types (SPTs) form a grammar for ...
- ArticleSeptember 2004
Strongly typed heterogeneous collections
Haskell '04: Proceedings of the 2004 ACM SIGPLAN workshop on HaskellPages 96–107https://doi.org/10.1145/1017472.1017488A heterogeneous collection is a datatype that is capable of storing data of different types, while providing operations for look-up, update, iteration, and others. There are various kinds of heterogeneous collections, differing in representation, ...