ProgLog Pages |
ProgLog /
WorkshopSpring11Program for the upcoming ProgLog workshop.
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
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
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
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
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:
by Stevan Andjelkovic
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
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)
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. |