Haskell Symposium 2022
| title | author | length |
|---|---|---|
| Welcome | Nadia Polikarpova | 04m |
Short welcome and program highlights: an immediate keynote on ultrabike effects (GitHub) and tomorrow a keynote from the Haskell Foundation about what’s next… | ||
| PC Chair Report | Nadia Polikarpova | 06m |
Program committee experiments remove the no early round option and introduce a separate abstract deadline to start reviews sooner. Submissions: 22 abstracts… | ||
| Industrial Strength Laziness: What's Next? | David Thrane Christiansen | 47m |
Argues that Haskell moved from a niche idea to industrial-grade tools and now needs better interactive tooling: concrete proposals include richer Haskell… | ||
| GHC Proposal Presentations | Joachim Breitner, Gergő Érdi, Andreas Klebinger, Matthías Páll Gissurarson | 01h 30m |
Four concrete GHC proposals get short technical pitches and status updates: partial type synonyms let type synonyms contain wildcards that elaborate into extra… | ||
| Open Transactional Actions: Interacting with non-transactional resources in S... | André Rauber Du Bois, Samuel da Silva Feitosa, Gerson Geraldo Homrich Cavalheiro, Rodrigo Geraldo Ribeiro | 27m |
Open Transactional Actions (OTAs) extend STM Haskell to run IO inside transactions while registering runOT/liftIO/register commit and abort handlers, and they… | ||
| Oregano: Staging Regular Expressions with Moore Cayley Fusion | Jamie Willis, Nicolas Wu, Tom Schrijvers | 23m |
Oregano implements regular expressions as Moore machines with a Cayley/CPS compilation pipeline and staged meta-programming to emit specialized matcher code… | ||
| Cause and Effect(s): Towards a More Programmable Haskell | Rob Rix | 01h 00m |
Argues Haskell should be designed around effects, documents building the semantic toolchain and the fused-effects library, and recounts hitting severe… | ||
| Investigating Magic Numbers: Improving the Inlining Heuristic in the Glasgow ... | Celeste Hollenbeck, Michael F. P. O'Boyle, Michel Steuwer | 18m |
Explores changing GHC’s hard-coded inliner “magic numbers” by turning ten tuning constants into parameters, compiling GHC with different settings and running a… | ||
| How to Safely Use Extensionality in Liquid Haskell | Niki Vazou, Michael Greenberg | 31m |
Shows that the naive functional extensionality axiom in Liquid Haskell is inconsistent with semantic subtyping and polymorphism, gives a concrete… | ||
| Partial Type Constructors in Practice | Apoorv Ingle, Alex Hubers, J. Garrett Morris | 23m |
Proposes making partial type constructors explicit in Haskell by encoding well-formedness as constraints (implemented via type families and data-type contexts)… | ||
| Liquid Proof Macros | Henry Blanchette, Niki Vazou, Leonidas Lampropoulos | 21m |
Liquid Proof Macros is an extensible metaprogramming framework that uses Template Haskell to generate Liquid Haskell proof terms via a tactic-like DSL, and it… | ||
| Embedded Pattern Matching | Trevor L. McDonell, Joshua D. Meredith, Gabriele Keller | 26m |
Presents a concrete technique that lets host-language pattern matching produce embedded-language case expressions by representing user ADTs as a… | ||
| Eiger: Auditable, executable, flexible legal regulations | Alexander Bernauer, Richard A. Eisenberg | 27m |
Eiger implements a domain-specific language embedded in Haskell that encodes regulations as dependency graphs of facts, pairs a domain expert with an engineer… | ||
| Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell | Lykourgos Mastorou, Nikolaos Papaspyrou, Niki Vazou | 23m |
Mechanizes coinductive proofs inside Liquid Haskell by encoding coinduction two ways: indexed coinduction (use a natural-number index to reduce stream equality… | ||
| A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures | Gershom Bazerman | 20m |
Claims that every traversable functor admits an infinite traversable instance and that an infinite traversal is productive iff the applicative used is of the… | ||
| Reasonable Agda is Correct Haskell: Writing Verified Haskell using agda2hs | Jesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman, Ulf Norell | 24m |
Tool agda2hs translates an expressive subset of Agda to readable Haskell by erasing dependent types and proofs using Agda's runtime irrelevance (erasure)… | ||
| nothing matches | ||