AIM9CodeSprint

• Schedule 3/12
  • Morning : Code Sprint
  • 12.00 -- Code Sprint while eating lunch
  • 14.30 -- Final Review
  • 16.40 -- Discussion on Future of Agda
  • 17.20 -- Non-CVS members leave the room, CVS members start restoring the room
  • 19.00 -- Last Dinner at the Hotel
• Documentation
  • Member: *Bengt, Yoshiki, Anton, Peter, (Nisse:Consultunt), Matsuno-san
  • Target:

1. Minimal
   1. How to download and install
   2. Ulf Tutorial
   3. How to use
   4. link to mailing list.
2. Make that 'Reference' usable, like, removing.
   • Progress:
     • 1128: Reorganized the top page, now the important information is in one-screen. Yoshiki: user guide, Nisse: applying screencast techonology, listing up most important libraries,
     • 1201: Cleaned up the Main Page; Fits in one page; Better Getting Started; MacOSX Installation Page (Shin-Cheng, use MacPorts; note for fonts); Swansea installation note to be updated; Quick Guide to the systems (Yoshiki, then edited by others); Most commonly used libraries (Nisse, needs more feedback); Soon(?) Agda and Lib released together; Most common key binding(Nisse)
     • 1202: Anton's Swansea material(Other Tutorials:Lecture Notes in Interactive Theorem Proving, Download:Installation Guide); Publications with all kinds of info and papers, Reference Manual Draft(Bengt); Fixed the implementation to remove awkward notes (Nisse); Improved OSX Instruction (Shin-Cheng); Example:MLTT, good for introducing Agda notation to those who know MLTT(Peter)((discussion on hiding elimination target families)); Translating Yoshiki's Japanese Tutorial to English (Matsuno-san);
     • 1203: A tool for translating xxx.agda to web pages, translation itself is easy, merging three drivers of typechecker into one (Nisse); Reference Manual improvement, introduction to Agda and TT completely rewritten (Bengt); Continuing English-translation of Yoshiki's Japanese tutoalial, uploaded in a few days (Matsuno-san); On how to use the compiler in QuickStart section, but Windows agda is completely dead right now ... (Yoshiki); ((Need for describing command-line invocation? Is it necessary? Just two sentences in QuickStart section)); Instruction for updating Agda (Anton)

• Optimizing Agda Implementation
  • Member: *Nisse, Ulf, Makoto
  • Target: Loading xxx.agda in ?? minutes
  • Progress:
    • 1128:
      • Discussion on "erasure" strategies; erasig at type checking time and at runtime after compilation. Erasing type-arguments and irrelevant proofs at runtime; some prf erasable even at type checking;
  aproach 1 : (Pfenning)

                              A
                           -------
                            [ A ]

approach 2 : (erasable function type?)

               \   x   . t : ( x : A ) -> B
               \ [ x ] . t : [ x : A ] -> B
               \   x   . t : ?
     Investigating how much of "swimming up"
        (= instantiating ? above with Pi ? ?) is used.

• Optimization by down grading (MT trying to make windows-distribution with GHC-6.8.3)
• xxx.agda = Parser combinator library.

• 1201
  • Switching internal rep of Term: Inefficiency caused by 1. comparison of the same thing and 2. slow eval; Experiments on 1 (95% comparison on syntactically equal terms);
    • Plan Term will have Pointer structure for faster comparison and call by need.
    • Started: Painful process of changing the interface to Term more abtract; Done 123 / 177.
• 1202 Ulf continues to mash his brain. 20 more modules to go before compiling (before we know we have gained anything.)
• 1203
  • Ulf: It compiles, Type checks, some bugs left, when debuged will be 10times slower,
  • Summary: Infrastructure for the Plan on 1201 is taking forms. Now all the substitution is strict. Actual optimization on this infrastructure must follow quickly, since just puching the patch for infra slows Agda down a lot.
  • (Windows) Not solving the problem with process-1.0.1.1 + GHC-6.8.3, De-optimizing to Windows distribution with GHC-6.10.1 (Makoto)

• Integrated Verification framework using Agda compiler
  • Member: *Makoto, Yoshiki, (Ulf)
  • Target:

1. Simple Poorman's Integrated Verification framework
2. (Koens' embedded language-like tactics & interpreter)
   • Progress:
     • 1128: Nothing
     • 1201: Fixed experimental Basic Framework.
     • 1202: Spin instance almost done
     • 1203: Spin instance is done no testing yet, some library extension proposal (Makoto) ((agda IO layer for IO-program that terminate-checks.)) ((Translator from XXX.hs to XXX.agda wanted.))

• Agda for Specification
  • Member: *Okamoto, Peter, Anton, Bengt, Yoshiki, Kitamura, Lee-san, (Makoto)
  • Target:

1. State Transition Machine Specification Framework
2. Dines Bjorner Specification in Agda
   • Progress:
     • 1128: Planning. VDM examples to Agda. Vocabraries taken from a NL spec. Boiling pot example.
     • 1201: Translating Bjorner example. Started axiomatizing(?) vocabulary about sets using postulate.
     • 1202: Realising the problems (Yatabe-san, Kitamura-san), how can you make similar but differing terminologies(?) uniform?
     • 1203: Defining Bjorner example in Agda, Found an incorrect formal statement in Bjorner example (Okamoto-san); Discussion from yesterday continues (Yatabe-/Kitamura-san)

• First Order Modal Mu Calculus in Agda
  • Member: *Yoshiki, Okamoto
  • Target: Formalizing First Order Modal Mu Calculus formulas, inference rules, ...
  • Progress:
    • 1128: Nothing
    • 1201: Nothing
    • 1202: Nothing
    • 1203: FOM.agda
• Sized Types
  • Members: *Andreas, Ulf, Nisse
  • Target:

1. Positivity test for types
2. Sized codata
   • Progress:
     • 1128: Nothing
     • 1201: Discussion on sized types for coinduction; found unsound ... ; need more check.
     • 1202: Try understanding coinduction...(see Codata experiments)
     • 1203: Another idea on sized codata, started implementation, will be done next time...; Modulus of Conitnuity (continuous functions of the kind that consumes two to produce one etc., related to analysis, epsilon-delta, etc.);

• Universe Polymorphism, Universe Subtyping
  • Members: *Ulf, Andreas, Conor, Peter, Nisse
  • Target:
  • Progress:
    • 1128: Nothing.
    • 1201: Nothing. Hijacked by Optim.
    • 1202: Nothing. Still Hijacked by Optim.
    • 1203: Nothing. Lost out to Optimization.
• Coq-like bytecode-compilation during typechecking (cf.German to machine code)
  • Members: *Kato-san, Ulf, Andreas, Makoto
  • Target: get a plan. try utilising Agate effort.
  • Progress:
    • 1128: Reading Agda impl code. Figuring out where to insert the compilation phase. Just adding byte-code compiler may not be so effective. Need to use result from Optimisation group. A possibilities is to replace the definition of a Agda funtion by byte-code. (forming another idea ...)
    • 1201: Discussed use of higher-order values; found not so useful probably (interface file has to be first order).
    • 1202: STG.agda:Agda formaliztion of G-machine, adapting it to Library, use of intensional rather than boolean equality to make proofs simpler (Kato-san)
    • 1203: Almost finished STG.agda, One problem in the formalization, Compiler needs fresh names, Representation of a variable as a string needs to be changed.
• Programming Excersises
  • Members: *Conor, Nisse, Peter, Shin-Cheng, Hamana-san
  • Target:

1. Originating from Conor
   1. Miller style pattern unification
   2. Dyckhoff's algorithm for proof search in propositional int. logic.
   3. Reflective procedure for...
   4. Library for programming free monads
   5. Experiments on representations (in Agda) of dependent type theory
   6. Ornamenting plain data types to fancier ones
   7. Formalizing uniform continuity
2. Originating from Nisse
   1. IO and other Haskell library
   2. Containers, and Interface thereof
3. Graph representation
   1. Representation of graphs with general 'back edges'
   2. Investigate whether inductive recursion can be useful for that.
   • Progress:
     • 1128:
       • Conor: caused stackoverflow, extentional universe construction, data structure for Miller unification,
       • Graph: from the representation CList of cyclic list to the really cyclic coList (failing termination check), Conor solution with codata WHNF, on our way to build recursive structures.
     • 1201:
       • Down a hole: Uniform continuity coninued (Conor)
       • App of Graph rep Shin-Cheng, Hamana-san; arrows with loops; stuck at how to define circular structure; need to capture the body of fixpoint in types(< Nisse)
     • 1202:
       • Conor: Lots. The game model for uniformly continuous computation. Better understanding of its structure. Examples of the "Ornamentation." Ornament.agda (proven correct compiler for stack machine with one-line proof). 1. type Desc I of codes for data type definition. Positivity check turned off. 2. Codes for Ornamentation given a Desc I with plain I and a fancy J; each ornament giving Desc J with fancy J. List from Nat. 3. Algebras give rise to ornaments. Vec from List for free. 4. AOOAThm (the length of list gotten from vector is the original index) 5. Stack machine (indexed by initial / final heights); Desc of HCode, Code algebra HAlg indexed by heights, Ornamenting HCode with HAlg (codes indexed by the semantics), writing compiler for exps with codomain this fancy indexed code type, typechecking ok = compiler is correct, AOOAThm says the the forgetful compiler to the plain code is also correct.
       • Hamana-san+Takai-san: Translating cyclic terms to a syntax for Arrows with loops. Had been done before in Haskell using laziness. Defining the combinator "loop" in Agda was difficult. Takai-san have a variant requiring initial input, but the translation came out slightly incorrectly, with extra delay. Still looking for the right "loop"; Tree raversing using "zippers", substitution of shape-indexed trees; Found fancy indexing and ornamentation useful to find bugs.
     • 1203: A simpler treatment of data structure for Miller unification, Unif.agda (Conor); Zipper by differentiation (Hamana-san), DependentTree.agda (Hamana-/Takai-san)

• Agda for Coq users (Completeness of FOL etc.)
  • Members: *Lee-san,
  • Target:

1. retarget the coq formalization to Agda
2. Complain about Agda from Coq users' viewpoint.
   1. Rebut the Coq-is-better argument.
   • Progress:
     • 1128: Followed Ulf Tutorial, Found Agda simpler than Coq, Adding comments to Ulf Tutorial.
     • 1201: Not much in terms of comments; Own coding (a lemma, comparing induction using pattern matching and using elimination(?); can loose sight of the whole when constructing large ind.proofs (= recursive funcs))
     • 1202: Getting familiar with Agda. Use of placeholders and pattern matching are very nice. Building large recursive proofs/functions are not that difficult (as I thought yesterday) once you get used to various helps. There should be a tutorial about how to use placeholders.
     • 1203: Formalizing the languagage of FOL. Herbelin style. Found Agda Very Good. Particularly Dependent Pattern matching. ((Inversion lemmas not needed)) Good for programmer. ? for logician. ((With indexed, deBruin terms, lots of verification conditions would not be needed, comparison?))((Making relations to functions would delegate more to computation))

• Experiments with Codata
  • Members: *Anton, (Conor), Nisse, Andreas, Peter, Shin-Cheng, Hamana-san
  • Target: Investigate how Setzer way relate to the current Agda implementation.
  • Progress:
    • 1128: Discussion on how to mix recursive and co-recursive functions, and the mixing rec / co-rec clauses of one functions. (-> codata experiments)
    • 1201: Implementation started: Mixed data / codata recursion (Andreas, ...); Small experiments (Anton)
    • 1202: mutual rec func & corec func can be done now (Andreas, ...); Examples(Stream Transducer; WHNF a -> El a); ((Needs for a policy and instruction on how to contribute examples on Agda Wiki; Doubtful if it's going to become a jumble?; Some organization needed; ))
    • 1203: Implemented the contents of the talk (Anton).
• Emacs-mode improvement
  • Member: Nisse, Makoto, U
  • Progress
    • 1201: Fixed emacs-mode (Nisse; c-c c-l for load; middle-button click for jumping to the definition site; default for normalize or not swapped.)
    • 1202 Better highlighting when there's type errors, shorter key-strokes & menues, invoking compiler within emacs. NOTE: executables now produced in the current directory by default, Interface file written also for the toplevel file (Nisse) ; hightlighting bug fix for Windows (M); ((discussion on the need for describing the "update" procedure - to be added to Download page))
• Discussion on Future of Agda
  • Short Term
    • Release of a new version. Agda-2.2.0, lib-0.1
    • More contribution to library wanted in a hurry, before the lib-0.1
    • Some place to hold (a jumble of) examples.
      • Candidate 1: Agda/Examples, have a page on Wiki
      • Candidate 2: Haskell like 'code snipet' page, Coq like Contribution page
  • Medium Term
    • Preventing Wiki rot.
    • Will there be a next time? Next June. <- things should happen before then. (sized codata, the new usable infrastructure)
    • Ideas from non-developers?
      • Conor: More shoplifting from Epigram-2. Observational Equality,...
      • Anton: More on Agda for Specification thingy? -> Yatabe-san:
      • Yatabe-san: More translators etc. that connect Agda with other tools are wanted.
  • (Long Term at Dinner)
• Next AIM
  • AIM10: In Goteborg, 4 June -- 10 June, 2009
    • organization: 1/2 day lecture 1/2 day code spint from the beginning. Lectures open to public, codesprint for serious participants only, notification on agda mailing list, but not on types mailing list, say.
  • AIM11: In Osaka(or somewhere in Japan), 11 January -- 15 January, 2010
    • German uni are in a teaching period. (Andreas)