Games and constructive type theory

One reason that I keep returning to Shahid Rahman’s work is that I’m reminded by the Academia app. However, I have a hard time making it through his articles. In part, this is because I don’t always know how to relate his work to game semantics in computer science, game theory (with probability as a one-player game), Peirce’s work as developed by Pietarinen, or Mellies work on linking homotopy type theory and differential linear logic.

It would be valuable for me to develop a better understanding of game semantics (Pietarinen calls them game-theoretic semantics) and decision theory (i.e. games between a player and the environment).

Rahman mentions empirical content in constructive type theory. In Shafer’s game theoretic interpretation of probability, the third player is the environment, which somewhat plays the role of empirical content.

Mathematical co-design

Andrea Censi, one of Spivak’s collaborators, has been working on expanding the co-design framework that appears in Seven Sketches. He is Deputy Director for the Institute for Dynamical Systems and Control at One of his Ph.D. students, Gioele Zardini, appears to have taken the lead role in this development.

The co-design approach tries to leverage compositionality to make the design of complex systems easier.

Design, or synthesis problems, are at the core of all

“Design, so construed, is the core of all professional training”

Engineering is about tradeoffs.

Energy systems have important interactions

Co-design, despite it’s name, is not short for collaborative design.

The category of codesign problems is modeled as a traced monoidal category