Recent Changes - Search:
FP /

Some Recent Research in the "Generic Programming Group"

Patrik Jansson, fp.st.cse.chalmers.se

Chalmers University of Technology and University of Gothenburg

Our "Generic Programming" Toolbox

  • Types (type systems, PTS)
  • Functional programming (lambda calculi)
  • Datatypes (based on Category Theory)
  • Language processing (grammars, parsing, transforming, ...)
  • Dependent types (inductive families, Martin-Löf type theory)
  • Executable specifications (QuickCheck testing, Agda proving, FOL-tools)
  • Domain Specific Languages (often embedded in Haskell)

Recent papers / projects

  • Papers:
    • ParaDep: Parametricity for Dependent Types, ICFP 2010
    • PolyTest: Testing Polymorphic Properties, ESOP 2010
    • Concepts: C++ Concepts = Haskell Type Classes, JFP 2010
    • VulnModel: Monadic Dynamical Systems (a DSL for vulnerability modelling), DSL 2009
    • AoPAgda: Algebra of Programming in Agda, JFP 2009
  • Projects:
    • FunC: VR proj. on Putting FP to work using DSLs
    • GSDP: EU proj. on DSLs for Global Systems Modelling

Who are we

Patrik Jansson, PhD 2000 "Polytypism", Assoc. Prof. 2004

  • Former students
    • Ulf Norell, PhD 2007 (now PostDoc & Quviq)
      • Agda (dependent types)
    • Nils Anders Danielsson, PhD 2007 (now PostDoc Nott.)
      • "Functional Program Correctness Through Types".
  • Current students
    • Jean-Philippe Bernardy, PhD stud. 2007--
      • Industry exp., Yi, Concepts, LazyParse, PolyTest, ParaDep
    • Cláudio Amaral, PhD stud. 2010--
      • Erl2Why: Dynamic lang. verification using the Why tool
    • Jonas Duregård, PhD stud. 2010--
      • Agata (Generate QC generators), BNFC + Quasiquoating
  • International collaborators:
    • Utrecht, Nottingham, Oxford, Potsdam, Indiana, Taiwan

Overlapping interests (my guess based on abstracts):

  • Taha / Patrik+GSDP: Hybrid modelling, high-level modelling
  • Inoue / Patrik+Jonas?: Reasoning about staged programs
  • Brauner / Patrik+JPB?: Proof refactoring