Recent Changes - Search:
FP /

PapersToWrite

Papers you plan to write

Mary

  • Mary: JFP paper about search and combinators for pp. Work left: polishing of code, writing
  • Mary: history of func. langs. and hardware design paper (with Chinese co-author). Where: no idea! Work left: much polishing.
  • Mary+Koen+Joel: A DSL for GPU programming. Where: abstract to DCC by Nov. 5. Final paper: DAMP?? What is deadline for that?

Patrik

Published:

See Papers.

Submitted:

To be done:

  • Patrik with Marcin Benke?: Explaining generic programming techniques by their semantics or Build your own Universe An idea from the work on the CompLib paper a more detailed comparison of a few simplified generic programming approaches by implementing their semantics in a common framework (Agda). Can also be seen as a follow-up on the paper "Universes for Generic Programs and Proofs in Dependent Type Theory".
  • Patrik: Algebra in Agda Something on working with algebraic structures (semirings, commutative algebras, etc.). Nils Anders has a library with many nice definitions and the notation for equational proofs should be advertised more.
  • Patrik: MonadLaws Use techniques from Fast and Loose Reasoning and/or CoverTranslator to prove(?) that there is no StateMonad in Haskell. (Some results about which laws don't hold have been found by using QuickCheck with Nils Anders ChasingBottoms library. Koen has tried some things using hand-translation to FOL.)
  • Patrik: CoverTranslator / QuickProof Continue work on translating Haskell to FOL and report on the results. A draft by Gregoire Hamon describing CoverTranslator is available, but the implementation was not in sync with that and has been improved afterwards (but still does not work as intended).

Koen

(Koen says: I have moved all these "todos" into a Todoist account and will not update these regularly anymore)

  • Koen: "Journal paper about Paradox". Where: Journal of Automated Reasoning. When: Jan 2008. Work left: Finish the new version of Paradox, writing.
  • Koen: "Finding Finite Sorted Models using Incremental SAT". Where: IJCAR. When: Jan 2008. Work left: Implement this in Paradox.
  • Koen: "Tutorial on QuickCheck". Where: Journal of Functional Programming. When: Jan 2008. Work left: Just the writing.
  • Koen: "Lazy SAT Monad". Where: Journal of Functional Programming (pearl?) / some other journal. When: ASAP. Work left: Find example applications, writing.
  • Koen+Hans: "Finding Counter Examples in Inductive Verification". Where: Conference TAP. Work left: Do some more QuickCheck hacking, writing.
  • Koen+Hans+John+Thomas: "Testing Formally Verified Algorithms". Where: Some journal. When: ASAP. Work left: Just the writing.
  • Koen: "Paper on Equinox". Where: IJCAR. When: Jan 2008. Work left: Just the writing.
  • Koen: "Paper on Approximation Models". Where: IJCAR. When: Jan 2008. Work left: Find more examples, implement model visualization, writing. (This is possibly the same paper as the one above.)
  • Koen: "AC Handling in MACE-style model finding". Where: IJCAR. When: Jan 2008. Work left: Implement and evaluate, writing.
  • Koen(+Thierry?): "Expressing Transitive Closure for Finite Domains in Pure First-Order Logic". Where: IJCAR/JAR. When: Jan 2008. Work left: Just the writing.
  • Koen+Chen: "Instance-based Theorem Proving is not so bad". Where: IJCAR?/JAR?. When: ASAP. Work left: Just the writing.
  • Koen+Niklas: "MiniSat's Incremental API". Where: Some SAT conference (IJCAR?). When: ASAP. Work left: Find a good example, writing.
  • Mary+Koen+Niklas: "Temporal Induction". Where: Some journal. When: ASAP. Work left: Investigate what to write, implement model checker, writing.
  • Koen+Mary: Tutorial on SAT and induction for SAT session at WODES08. Due around Jan. 25 2008 so getting urgent!
  • Koen+JWR: "Semantics of GSTE". Where: Logical Methods in Computer Science Journal. When: In the pipeline. Work left: None.