TyDe 2022
who it's for
type system researchers, dependently typed programmers, programming language designers, Agda developers, Idris2 developers, verification engineers, tool builders
topics
normalization by evaluation extensions; elaborator reflection generic programming; tile-based structure editing; generic trees in Agda; dead binding elimination for intrinsically typed syntax; algebraic refinement-type inference; dependently typed table schemas; Hoare-style refinement types and weakest preconditions; dependently typed control effects; syntactic sharing and call-by-need; cyclic mu calculus coherence; grammar inference via refinement types
| title | author | length |
|---|---|---|
| Normalization by Evaluation with Free Extensions (Extended Abstract) | Nathan Corbyn, Ohad Kammar, Sam Lindley, Nachiappan Valliappan, Jeremy Yallop | 15m |
Claim: augmenting normalization-by-evaluation with free extensions (frex) produces a single generic NbE algorithm for simply typed lambda calculus with… | ||
| Syntax-Generic Operations, Reflectively Reified (Extended Abstract) | Tzu-Chi Lin, Hsiang-Shang Ko | 16m |
Ports a core part of Allais et al.'s datatype-generic library into a new framework that uses Agda elaborator reflection to reify generic constructions into… | ||
| tylr, a tiny tile-based structure editor | David Moon, Andrew Blinn, Cyrus Omar | 19m |
A tiny prototype editor implements tile-based editing that disassembles terms into tiles and shards, uses a grouter and backpack to maintain convex shapes and… | ||
| Computing with Generic Trees in Agda | Stephen Dolan | 17m |
Shows that a small tweak to W-types makes generic tree definitions compute in Agda: replace function-indexed places with a mix of finitary tuples and labeled… | ||
| Provingly Correct Optimisations on Intrinsically Typed Expressions (Extended Abstract) | Matthias Heinzel | 13m |
Implements dead binding elimination for intrinsically typed syntax trees by annotating each subexpression with a live-variable subcontext and using… | ||
| Structural Refinement Types | David Binder, Ingo Skupin, David Lawen, Klaus Ostermann | 13m |
A lightweight refinement-type system and inference algorithm extends algebraic subtyping with rules from polymorphic variants to infer precise refinements… | ||
| Idris2-Table: Evaluating dependently-typed tables with... (Extended Abstract) | Robert Wright, Michel Steuwer, Ohad Kammar | 12m |
Built an Idris 2 library that encodes table schemas as dependent types and implements the Brown Benchmark for Table Types examples and programs, covering… | ||
| A Hoare-Logic Style Refinement Types Formalisation | Zilin Chen | 16m |
Presents a Hoare-triple style formalisation of refinement types implemented in Agda that interprets object terms shallowly and uses Agda’s type theory as the… | ||
| Towards Dependently-Typed Control Effects (Extended Abstract) | Youyou Cong, Kenichi Asai | 12m |
Design of a dependently-typed language with delimited control operators includes a purity restriction that types may depend only on pure terms and a selective… | ||
| On the power of syntactic methods: It is all syntax after all… | Amr Sabry | 12m |
Argues that many tricky operational problems become simple once the store and sharing are treated as syntax, demonstrates a concrete binding in evaluation… | ||
| Mu tilde (re)cycled | Pierre-Louis Curien | 17m |
Proves coherence for cyclic operads by building a mu calculus that merges two decomposition syntaxes, showing every composition order yields the same… | ||
| Toward Grammar Inference via Refinement Types (Extended Abstract) | Michael Schröder, Jürgen Cito | 12m |
Prototype system converts Python ad hoc parsers into a small lambda IR called Panini IR and infers precise refinement types, then solves unknowns using a… | ||
| Contextual Algebraic Theories: Generic Boilerplate beyond Abstraction | Andreas Nuyts | 12m |
Menkar faces massive duplicated boilerplate across renaming, substitution, normalization and pretty‑printing; the proposal defines Contextual Multisorted… | ||
| nothing matches | ||