Agda Implementors' Meeting XXIII progress summary

Wednesday 20 April

• Jesper: Found bug when using rewriting, plan to fix it.
• Ulf, Nisse, Guillaume, Andreas, Victor, Shayan: talked about do-notation, layout and copatterns. Decided that "lambda where" is good notation for a layout-aware pattern-matching lambda.
• Conor, Andreas, many others: Discussed cumulativity. Will experiment with using universe constraints instead of lsuc, lmax.
• Ulf: pushed idiom-brackets.

Thursday 21 April

• Ulf: flexible module parameters
• Andreas: Overloaded record fields
• Jesper: Higher Order REWRITING
• James, Fred, Guillaume: Typechecking despite termination check failure
• Henning: Adding codata, bisimulation and up-to techniques to the standard library

Friday 22 April

• Ulf: fixing bugs related to flexible module parameters
• Nisse: Module names are hashed, turns out the hashing function is not injective (exploit)
• Andrea: Experiments towards Cubical TT in Agda using BUILTINs and PRIMITIVEs
• Jesper: Experiments towards Cubical TT in Agda using REWRITE rules
• Andreas: Considerations on the ordinal iterations necessary to take the fixpoint of a strictly-positive indexed family
• Guillaume, Fred: Further work on non-fatal errors.

Saturday 23 April

• Andreas: Copattern matching with overloaded projections now also works (issue 1944)
• Conor: a formal language for multi-sorted syntaxes with binding and their typing rules
• Jesper: a logo for Agda
• Fred, Guillaume: Displaying aggregated errors in the emacs buffer.
• Henning: Structure of the standard library regarding Codata

Monday 25 April

• Andrea: Cubical-in-Agda: J now computes. Cannot yet do coercion, or handle inductive families. Time for equality-agnostic inductive families?
• Ulf: Closer to a working implementation of flexible module parameters. 40 39 30 24 failing test cases to go.
• Bob: Demo of Foveran, a language with a universe of descriptions of data types.
• Victor: Support for more literate code formats:
  • split up literate code support from lexer
  • added support for the rst format
  • mostly works, but some highlighting problems with identifiers
• Victor: some logo suggestions
• Jesper: fixed another REWRITE bug related to interaction with the constraint solver.
• Nisse: an optimisation.
• Andreas: Still working on overloaded projections; a few things cannot be fixed due to lack of postfix projection syntax, so maybe introduce that as well?
• Guillaume, Fred: started refactoring warnings.
• Edwin: looked at Nisse's challenge in Idris.

Tuesday 26 April

• Jesper: documentation code-sprint on indexed data types, strict positivity, pattern-matching (including dot and absurd patterns)
• James: Normalisation by Evaluation in the Delay monad: proving termination, soundness and completeness independently