Recent Changes - Search:

ProgLog Main


ProgLog Pages


edit SideBar

WorkshopSpring11

Program 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
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((X1/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.

Related blog post.


Universes for data

  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.

Slides


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.

Edit - History - Print - Recent Changes - Search
Page last modified on March 07, 2011, at 08:38 PM