Skip to content

Latest commit

 

History

History
46 lines (35 loc) · 1.77 KB

README.md

File metadata and controls

46 lines (35 loc) · 1.77 KB

Discrete Exterior Zoo

This is a repository for a research project that aims to

  • develop a type-theoretical model of discrete exterior calculus (see the related publications),
  • formalize the model with the Coq proof assistant (see the fowl component),
  • extract OCaml code from the proof-relevant parts of the formalization (see the camel component),
  • link the extracted code with an existing numerical solver (see the truffle component),
  • implement a user interface for the resulting system (see the snake and turtle components),
  • define a protocol and an architecture for distributing and extending it (see the ape and flower components and the associated fur, scales, shell and spores components) and
  • accompany it with utility libraries (see the ungulate, reptile and fungus components).

The code in this repository is free software and, as such, licensed under

  • the GNU General Public License version 3 or later.

The development of this project

  • started around 2018-05-01,
  • continues as of 2021-08-01 and
  • is expected to reach a usable state by 2022-05-01.

Currently, the authors of this project are

  • Jukka Räbinä, who works on the truffle component at IQM Finland, and
  • Sampsa Kiiskinen, who works on all the other components in the Faculty of Information Technology at the University of Jyväskylä.

Over the course of the project,

  • Sampsa Kiiskinen has been partially funded by
    • the Jane and Aatos Erkko Foundation grant 170015 and
    • the University of Jyväskylä Graduate School and
  • Jukka Räbinä has been partially funded by
    • the Academy of Finland grants 259925, 260076 and 295897 and
    • the European Research Council advanced grant 320773.

Stay tuned for other equally useful facts about this project.