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 3024 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
Powered by PmWiki