Objectives

• Track A: Artificial Intelligence and Symbolic Computation (AISC) (co-chairs: John A. Campbell, Jacques Carette)
• Track B: Calculemus (chair: Gabriel Dos Reis)
• Track C: Digital Mathematical Libraries (DML) (chair: Petr Sojka)
• Track D: Mathematical Knowledge Management (MKM) (chair: Makarius Wenzel)
• Track E:Systems & Projects (chair: Volker Sorge)

• Yannis Haralambous, Département Informatique, Télécom Bretagne
• Conor McBride, Department of Computer and Information Sciences, University of Strathclyde
• Cezar Ionescu, Potsdam Institute for Climate Impact Research:
  
  Increasingly correct scientific programming

  Dependently typed languages promise an elegant environment for programming from specifications: the properties that a program should satisfy are expressed as logical formulas and encoded via the Curry-Howard isomorphism as a type, a candidate implementation should be a member of this type, and the type checker verifies whether this is indeed the case. But sometimes, the type checker demands ``too much'': in particular, in scientific programming, it often seems that one must formalize all of real analysis before writing a single line of useful code. Alternatively, one can use mechanisms provided by the language in order to circumvent the type checker, and confirm that ``real programmers can write Fortran in any language''. We present an example of navigating between these extremes in the case of economic modeling. At first, we use postulates in order to be able to reuse code, and achieve a kind of conditional correctness (for example, we can find a Walrasian equilibrium if we are able to solve a convex optimization problem). We then remove more and more of the postulates, replacing them with proofs of correctness, by using interval arithmetic methods.

Workshops & Doctoral Programme