# WorkshopSpring11

Program for the upcoming ProgLog workshop.

- When: on March 8, 2011
- Where: Ågrenska Villan, on Högåsplatsen 2

09:00-10:00
*A pointfree theory of partial continuous functionals*

by Helmut Schwichtenberg

10:00-10:30 Coffee break

10:30-11:15
*Formalization of Rings with Explicit Divisibility in Type Theory*

by Anders Mörtberg

11:15-12:00
*Algebraic numbers and Newton theorem*

by Bassel Mannaa

12:00-13:30 Lunch

13:30-14:15
*Bag Equality via a Proof-Relevant Membership Relation*

by Nils Anders Danielsson

14:15-15:00
*Universes for data*

by Stevan Andjelkovic

15:00-15:30 Coffee break

15:30-16:15
*A Theory of Parametric Polymorphism*

by Jean-Philippe Bernardy

16:15-17:00
*A computational interpretation of parametricity*

by Guilhem Moulin (joint work with Jean-Philippe Bernardy)

19:00- Dinner at Linné Terrassen, on Linnégatan 32

*A pointfree theory of partial continuous functionals*

by Helmut Schwichtenberg

*Abstract*

Kreisel's density theorem says that every (consistent) formal neighborhood (i.e., finite partial functional) can be extended to a total one. Since the formal neighborhoods form a basis of the Scott topology of partial continuous functionals, this expresses that the total ones are dense. We propose to view abstract functionals as ideal objects or "points", seen as limits of their finite approximations, i.e., formal neighborhoods. From this point of view the study of formal neighborhoods becomes a foundational issue. We propose a formal such theory (a kind of extended arithmetic), and take the density theorem as a test case for its appropriateness.

*Formalization of Rings with Explicit Divisibility in Type Theory*

by Anders Mörtberg

*Abstract*

I will discuss recent work in formalizing the theory of rings with explicit divisibility using the SSReflect extension to Coq. A ring has explicit divisibility if it has a divisibility test that produces a witness, i.e. if a|b then it should (explicitly) give x such that b = xa. Rings with explicit divisibility that has been considered are GCD, Bézout and Euclidean rings, the standard examples of these are Z and k[x] (polynomials in one variable over a field). I will also discuss work on implementing and formalizing algorithms for computing the Smith normal form of matrices which is a generalization of Gaussian elimination for rings with coefficients from a PID instead of a field.

*Algebraic numbers and Newton theorem*

by Bassel Mannaa

*Abstract*

Newton theorem states that for a field k of zero characteristic, the
algebraic closure of the field k((X)) is the union of k((X^{1/m})) over
all positive integers m. I will present the work we have done so far
to obtain a constructive version of this theorem.

*Bag Equality via a Proof-Relevant Membership Relation*

by Nils Anders Danielsson

*Abstract*

Two lists are "bag equal" if they are permutations of each other, i.e. if they contain the same elements, with the same multiplicity, but perhaps not in the same order. I will discuss a definition of bag equality which I have found to be quite useful in practice. The definition has some nice properties:

- It generalises easily to arbitrary containers, including types with infinite values, such as streams.
- By using a small variant of the definition one gets
*set*equality instead, i.e. equality where neither multiplicity nor order matters. Many preservation proofs can be performed uniformly for both bag and set equality at the same time. - Many bag (and set) equalities can be proved using a form of equational reasoning.

by Stevan Andjelkovic

*Abstract*

I'll talk about what I've been looking at during my MSc thesis work, namely; how one can make use of the universe construction to avoid various forms of code duplication.

*A Theory of Parametric Polymorphism*

by Jean-Philippe Bernardy

*Abstract*

In the talk I will present the main points of the theoretical part of my thesis, which revisits the well-known notion of parametric polymorphism within type-theories with dependent types. I will show how the meaning of polymorphic, possibly dependent, types can be reflected within dependent type-theory itself, via a simple syntactic transformation. I will also examine how the translation relates to various specific features of type-theory, such as computational irrelevance.

*A computational interpretation of parametricity*

by Guilhem Moulin (joint work with Jean-Philippe Bernardy)

*Abstract*

I'll show how Reynold's abstraction theorem can be internalized (that is, both expressed and proved in the calculus itself) in an extension of the Calculus of Constructions with proof irrelevance and a special parametricity rule (with a computational content). I'll also present a few properties, and give the flavor of some of their proofs, that our system possesses hopefully e.g., Church-Rosser's and strong normalization.