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((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.
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.