Powered by
5th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2020),
August 23, 2020,
Virtual Event, USA
5th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2020)
Frontmatter
Welcome from the Chairs
Welcome to the 5th ACM SIGPLAN International Workshop on Type-Driven
Development (TyDe'20), co-located with the International Conference on Functional
Programming (ICFP 2020). The workshop aims to show how static type information may
be used effectively in the development of computer programs.
TyDe is a merging of two previous workshops: the Workshop on Dependently Typed
Programming and the Workshop on Generic Programming. These two research areas
have a rich history and bridge both theory and practice. Novel techniques
explored by both communities have gradually spread to more mainstream
languages. This workshop aims to bring together leading researchers and
practitioners in generic programming and dependently typed programming from
around the world, and features contributions capturing the state of the art in
these important areas.
The call for submissions sought both full papers (up to 12 pages, published in
the ACM Digital Library) and extended abstracts (up to 2 pages, not formally
published but posted on the workshop webpage). Each submission was evaluated by
at least three members of the program committee: full papers for the novelty
and significance of their results, and extended abstracts for relevance and
interest to the TyDe community. We received 4 full papers and 7 extended
abstracts, of which 2 and 7 respectively were accepted. The submission
period overlapped substantially with the beginning of the COVID-19 pandemic,
which likely contributed to a lower normal number of submissions compared
to previous years. Nevertheless, the submissions that we received presented
fascinating new ideas and results and we are pleased to be able to put together
an excellent online program.
Papers
Strongly Bounded Termination with Applications to Security and Hardware Synthesis
Thomas Reynolds,
William L. Harrison,
Rohit Chadha, and
Gerard Allwein
(University of Missouri, USA; Oak Ridge National Laboratory, USA; US Naval Research Laboratory, USA)
Termination checking is a classic static analysis, and, within this focus, there are type-based approaches that formalize termination analysis as type systems (i.e., so that all well-typed programs terminate). But there are situations where a stronger termination property (which we call strongly-bounded termination) must be determined and, accordingly, we explore this property via a variant of the simply-typed λ-calculus called the bounded-time λ-calculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating strongly-bounded termination and BTC are described as well.
@InProceedings{TyDe20p1,
author = {Thomas Reynolds and William L. Harrison and Rohit Chadha and Gerard Allwein},
title = {Strongly Bounded Termination with Applications to Security and Hardware Synthesis},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--10},
doi = {10.1145/3406089.3409029},
year = {2020},
}
Publisher's Version
Practical Dependent Type Checking using Twin Types
Víctor López Juan and
Nils Anders Danielsson
(Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)
People writing proofs or programs in dependently typed languages can
omit some function arguments in order to decrease the code size and
improve readability.
Type checking such a program involves filling in each of these
implicit arguments in a type-correct way.
This is typically done using some form of unification.
One approach to unification, taken by Agda, involves sometimes
starting to unify terms before their types are known to be equal: in
some cases one can make progress on unifying the terms, and then use
information gleaned in this way to unify the types.
This flexibility allows Agda to solve implicit arguments that are
not found by several other systems.
However, Agda's implementation is buggy: sometimes the solutions
chosen are ill-typed, which can cause the type checker to crash.
With Gundry and McBride's twin variable technique one can also start
to unify terms before their types are known to be equal, and
furthermore this technique is accompanied by correctness proofs.
However, so far this technique has not been tested in practice as
part of a full type checker.
We have reformulated Gundry and McBride's technique without twin
variables, using only twin types, with the aim of making the
technique easier to implement in existing type checkers (in
particular Agda).
We have also introduced a type-agnostic syntactic equality rule that
seems to be useful in practice.
The reformulated technique has been tested in a type checker for a
tiny variant of Agda.
This type checker handles at least one example
that Coq, Idris,
Lean and Matita cannot handle, and does so in time and space
comparable to that used by Agda.
This suggests that the reformulated technique is usable in practice.
@InProceedings{TyDe20p11,
author = {Víctor López Juan and Nils Anders Danielsson},
title = {Practical Dependent Type Checking using Twin Types},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {11--23},
doi = {10.1145/3406089.3409030},
year = {2020},
}
Publisher's Version
proc time: 0.41