ProgLog Meetings in 2006
Past meetings of 2006.
Date 
Speaker 
Title 
Extra 

Dec 15 
Sergei Soloviev 
Nonstandard reductions in typed lambdacalculus with inductive types and normalization properties, at 11.15, in room 5453 
abstract 
Dec 13 
Thomas Hallgren 
Operating system construction in Haskell and some ideas on using dependent types 
abstract, ICFP2005 paper 
Dec 6 
Conor McBride 
Epigram 2: the core story, video seminar with AIST and Nottingham, at 9.00, in SGSR 
abstract 
Nov 29 
Nils Anders Danielsson 
A Simple Library for SemiFormal Verification of the Time Complexity of Purely Functional Data Structures 
abstract 
Nov 22 
Arnaud Spiwack 
Towards efficient computation in Coq 
abstract 
Nov 15 
Ana Bove 
Computation by Prophecy 
abstract 
Nov 8 
Ulf Norell 
A typesafe treatment of meta variables 
abstract 
Nov 1 
Aarne Ranta 
Compiling GF 
abstract 
Oct 25 
Peter Dybjer 
The history of the identity type 
abstract 
Oct 18 
Bas Spitters 
Constructive analysis, types and exact real numbers. 
abstract, [Spitters], [O'Connor] 
Oct 11 
Thierry Coquand 
Getting Pi right in Set 
abstract, slides 
Oct 4 

meeting 

Sep 27 

No ordinary ProgLog meeting during AIM5 

Sep 20 
Thierry Coquand 
informal reports 
abstract 
Sep 13 
Fredrik Lindblad 
Finding Counterexamples and Proofs using Meta Variables in Functional Programs 
abstract 
Sep 6 
David Wahlstedt 
Dependent Type Theory with Parametric FirstOrder Data Types and PatternMatching 
abstract 
Aug 30 
Andres Sicard 
Hypercomputation 
abstract 
Aug 23 
Nils Anders Danielsson 
A definition of a dependently typed language as an inductiverecursive family 
abstract 
Jun 16 
Norio KATO 
Exploiting Type Information to Compile Agda into Haskell, video seminar with AIST, at 9.00 in video conf. room, AVcentralen, Vhouse 
abstract 
Jun 14 
Michael Hedberg 
Verifying Warshall's algorithm in Agda, room 6128 
abstract 
Jun 7 
Peter Dybjer 
Normalization by Evaluation for MartinLöf Type Theory with One Universe 
abstract 
May 31 
Patrik Jansson 
Testing properties of generic functions 
abstract 
May 10 
Ulf Norell 
Agda II  Take One, video seminar, at 9.00 in video conf. room, AVcentralen, Vhouse 
abstract 
May 3 

AISTcollaboration 

Apr 26 
Fredrik Lindblad 
Proof Search by Lazy Instantiation of FirstOrder Terms 
abstract 
Apr 12 
Bengt Nordström 
Interaction with a Proof Editor 
abstract 
Apr 5 
Andreas Abel 
Sized (Co)Inductive Types (With Applications to Generic Programming) 
abstract 
Mar 29 
Ana Bove 
General Recursion and CoInductive Types 
abstract 
Mar 22 
Thierry Coquand 
Typing Rules for Agda 2, video seminar with AIST, at 9.00 in video conf. room, AVcentralen, Vhouse 

Mar 15 
Jordi Saludes 
Generating natural language for mathematical exercises 
abstract, link 
Mar 15 
Tamara Rezk 
Certificate translation, at 10.15 in 5453 
abstract 
Mar 8 
Carlos Gonzalía 
Relations in Dependent Type Theory 
abstract 
Mar 6 
Masahiko Sato 
Abstraction and Substitution by FregeGentzen Approach, NOTE: irregular day and time: Monday, Mar 6, at 15.15, in 5453 
abstract 
Mar 1 

Meeting to discuss: VRapplications, webpages, TYPES workshop 

Feb 22 
David Wahlstedt 
Proving Reducibility of Recursively Defined Constants 
abstract 
Feb 16 
Danko Ilik 
Zermelo's wellordering theorem in type theory, Thursday, 11.00, ES63, Master's thesis pres 

Feb 8 
Ulf Norell 
Implicit arguments in Agda2 
abstract 
Abstracts of talks in 2006
Nonstandard reductions in typed lambdacalculus with inductive types and normalization properties, at 11.15, in room 5453
(Joint work with D. Chemouil and F. Barral)
Date: Dec 15
Speaker: Sergei Soloviev (IRIT, Toulouse)
Abstract:
One of well known difficulties encountered in the applications of proofassistants based on type theory is that many equalities that a user expects for granted are satisfied only extensionally (not supported by reduction mechanisms). We study some reductions that may be added preserving SN and CR property and ?transform? certain useful equalities into intensional w.r.t. the extended system. (For example, invertibility of some functions.) Main results concern simply typed lambdacalculus with inductive types. We consider isomorphisms between copies of inductive types, products, finite types. The problem of functoriality of a schema of an inductive type with parameters is studied. Some possibilities of generalization to the systems with dependent types are considered.
The talk is based on joint work with D. Chemouil (former ph.d. student) and F. Barral (ph.d. in progress).
Operating system construction in Haskell and some ideas on using dependent types
Date: Dec 13
Speaker: Thomas Hallgren
Links: ICFP2005 paper
Abstract:
First, I present "A Principles Approach to Operating System Construction in Haskell" (from ICPF 2005), where we describe a monadic interface (the H monad) to lowlevel hardware features that is a suitable basis for building operating systems in Haskell. Its behavior is specified in part by formal assertions written in a programming logic called PLogic.
While most memory safety requirements can be captured in the types of the H monad operations, and checked at compiletime, some checks (bounds checks) have to be deferred until runtime. So, second, I describe a little experiment using dependent types to move more checks to compiletime, further reducing the risk that programmer mistakes go undetected until runtime, and potentially also improving performance.
Epigram 2: the core story, video seminar with AIST and Nottingham, at 9.00, in SGSR
Date: Dec 6
Speaker: Conor McBride
Abstract:
Not much of Epigram 2 actually exists yet, but I can give you some idea of what it will be like, on the outside and on the inside. I'll give an overview of the system's structure, then focus on the key ideas and methods which are central to Epigram 2. The crucial idea, carrying over from Epigram 1, is to separate the source language from the core type theory, thus reducing the tension between the design imperatives of convenience for the former and simplicity for the latter.
I shall concentrate mainly on on our new core. We now distinguish syntactically between the terms whose types may be synthesised and those whose types must be prescribed. This choice has had a significant impact on the way we think about data in Epigram. Rather than equipping our system with the means to add new datatypes to our type theory, we directly add a universe of datatypes whose codes are themselves data.
This has been a team effort, thanks to Thorsten Altenkirch and his PhD students. Specifically, this talk is largely based on a collaboration with James Chapman and Peter Morris.
A Simple Library for SemiFormal Verification of the Time Complexity of Purely Functional Data Structures
Date: Nov 29
Speaker: Nils Anders Danielsson
Abstract:
Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. The associated time complexity analysis often requires careful attention to detail, and hence formalising it is valuable.
This work describes a simple library that can be used to formalise the analysis of a class of purely functional data structures. The basic idea is to use the type system to annotate all functions with the time required to compute their result. An annotated monad is used to combine time complexity annotations. The library has been implemented and used to analyse some existing data structures, for instance (parts of) the finger trees of Hinze and Paterson.
It is also sketched how amortised data structures analysed using the library can be automatically turned into worstcase ones.
Towards efficient computation in Coq
Date: Nov 22
Speaker: Arnaud Spiwack
Abstract:
With growing activity, the users of Type Theory tend to need more and more computation, both to use Type Theory as a reasonable programming language and to make proofs with a big computational content. I shall focus on the proof assistant Coq, and show how to use the existing structures (in particular the Virtual Machine) to add efficient natural numbers computation at a minimal cost. This is done in two mostly independant steps : the choices and constraint of representation inside Coq's virtual machine, and the representation seen by the user. In order to glue both together, we introduce a mechanism called "retroknowledge", whose main goal is to internalize into the theory (Coq's kernel) some meaningful parts of the user's developpement.
Computation by Prophecy
(Joint work with Venanzio Capretta)
Date: Nov 15
Speaker: Ana Bove
Abstract:
On one hand, we have the BoveCapretta (inductive) method to define partial and general recursive functions in type theory.
On the other hand, we have Venanzio Capretta's paper showing how one could use coinductive types to represent partiality in type theory. Can we combine both method and define a BoveCapretta (coinductive) method which has the advantages of both previous work?
Those of you who were at TYPES meeting in Nottingham might think you have already listen to this talk! But you are only partly right...
In the talk on Wednesday I will present a new method to represent general recursion and partiality in type theory using coinductive types which is much more efficient than the one presented by Venanzio at the meeting in Nottingham. I will also show how to prove that the recursive equations are still valid.
A typesafe treatment of meta variables
Date: Nov 8
Speaker: Ulf Norell
Abstract:
I will present the work Catarina and I have been doing on meta variables. There will be typing rules, examples, and live demos. See below for a more technical description of the problem we are solving.
In type theory the convertibility rule states that if t : B and A = B then t : A, where A = B means that A and B have the same normal form. To implement this rule a type checker can simply normalise A and B and check if the normal forms are equal. However, in the presence of meta variables this is no longer possible: A and B might contain meta variables preventing them from being normalised. Instead A and B are unified, possibly instantiating some of the meta variables. The unification can have three different outcomes:
yes  found a unique instantiation which makes A = B
no  no instantiation makes A = B
maybe  couldn't find a unique instantiation, but one could still exist
The troublesome case is the third one. In previous implementations of Agda the approach have been to accept t : A but remember the constraint A = B. The problem with this is that if a meta variable is later instantiated making A and B different you have an illtyped term t on your hands. Our solution is to replace t by a fresh constant c : A = t whose definition is only accessible if A = B.
Compiling GF
Date: Nov 1
Speaker: Aarne Ranta
Abstract:
GF is a grammar formalism, i.e. a special purpose programming language for writing grammars. It is a functional language with dependent types. A GF program (a grammar) is a declarative definition of a language, on a high abstraction level that improves grammar writing productivity.
To compile a GF grammar is to generate lowerlevel code that performs two computational tasks:
 linearization: take syntax trees to strings
 parsing: take strings to syntax trees
The talk gives an overview of the compilation process, as well as snapshots of some special problems, in particular
 the module system and separate compilation
 backend optimizations of grammars
 grammar checking as type checking
The history of the identity type
Date: Oct 25
Speaker: Peter Dybjer
Abstract:
I will talk about the history of the identity type. I will start with the letter of Howard to Kreisel in 1969, and will continue with the accounts of identity by Lawvere 1970, Scott 1970, MartinLöf 1971, 1972, 1973, 1979, and 1986. If time permits I will also say something about the more recent findings about the identity type.
Constructive analysis, types and exact real numbers.
(Joint work with Herman Geuvers, Milad Niqui and Freek Wiedijk)
Date: Oct 18
Speaker: Bas Spitters (Institute for Computing and Information Sciences, Radboud University, Nijmegen)
Links: [Spitters], [O'Connor]
Abstract:
We will discuss various aspects of computable/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real arithmetic varying from concrete implementations, representation and algorithms to various models for real computation. We then put these models in a uniform framework using realisability, opening the door for the use of type theoretic and coalgebraic constructions both in computing and reasoning about these computations. We will indicate that it is often natural to use constructive logic to reason about these computations.
Finally, I will scrupulously show the work of Russell O'Connor on the "FewDigits"implementation of exact real numbers in Haskell and Coq.
Literature:
* Constructive analysis, types and exact real numbers. (with Herman Geuvers, Milad Niqui and Freek Wiedijk) to appear in Constructive analysis, types and exact real numbers, special issue of Mathematical Structures in Computer Science (Bas Spitters, Herman Geuvers, Milad Niqui and Freek Wiedijk(eds.)) MSCS 2006.
http://www.cs.ru.nl/~spitters/editorial.pdf
* http://r6.ca/FewDigits/
Getting Pi right in Set
Date: Oct 11
Speaker: Thierry Coquand
Links: slides
Abstract:
After the discussions about "Pi in Set" at the last AIM5 I got new inputs from Peter and Andreas (and Klaus Aehlig). These suggest a systematic method, based on normalisation by evaluation, to prove the desired metaproperties of a type system with universes and strong conversion rules (eta conversion, but also surjective pairing or conversion rules for singleton types). It gives also an elegant way to program the conversion algorithm, which fits well with the current implementation of core agda.
I will present the formal system (type theory with universes with conversion as judgements), its PER semantics and the associated normalisation and conversion algorithms. I will then argue that, provided the proofs of correctness and completness of these algorithms are valid, this formal system should be the basis of Agda 2 (instead of the Logical Framework).
The slides are available.
informal reports
Date: Sep 20
Speaker: Thierry Coquand
Abstract:
This will be very informal. I will report quickly on a few things that I found interesting at some meetings I have just attended. I should present:
a surprising Haskell program, by Martin Escardo and Ulrich Berger, with which we can write, in a total way, universal and existential quantifications over an infinite data type (good approximation of the halting problem)
some examples by Helmut Schwichtenberg of program extractions in minlog (at least square root functions [1,4] > [1,2] extracted from a general lemma about existence of inverse functions)
the complete mechanization of Hessenberg's Theorem by Marc Bezem and Dimitri Hendriks (stating that Pappus axiom implies Desargues axiom), in type theory connected with a special firstorder prover
Finding Counterexamples and Proofs using Meta Variables in Functional Programs
Date: Sep 13
Speaker: Fredrik Lindblad
Abstract:
At my previous ProgLog presentation I described some experiments in adding meta variables to a functional language and doing search. The idea was applied on program verification by finding counterexamples for functional properties, and on finding proofs by implementing a proof checker. The search algorithm is based on two main ingredients; lazy instantiation and parallel evaluation.
I will continue on these two tracks and also discuss the relation to Curry, a functional logic language, in particular the concepts of narrowing and concurrent constraints.
Dependent Type Theory with Parametric FirstOrder Data Types and PatternMatching
Date: Sep 6
Speaker: David Wahlstedt
Abstract:
We present a variation of MartinLöf's logical framework with $\beta\iota$equality, extended with firstorder parametric data types and constants defined recursively with patternmatching. We use the \emph{SizeChange Principle for Program Termination} (C.S. Lee, N.D. Jones, A. BenAmram 2001) to justify the recursive definitions. This approach enables us to define new constants in a straightforward manner. Our contribution is a proof of normalization for the proposed system.
Hypercomputation
Date: Aug 30
Speaker: Andres Sicard
Abstract:
While the idea of an absolute computability (i.e. Turing machine computability), detached from logical, mathematical, physical or biological theories is hard to hold nowadays, the idea of a relative computability has progressively gained supporters, as shown by the establishment of an academic community around hypercomputation theory (i.e. computing beyond Turing machine's limit). In this talk we will show some hypercomputation models, the relation between hypercomputation and the ChurchTuring thesis, and our results on the possibility of hypercomputation based on quantum computation.
A definition of a dependently typed language as an inductiverecursive family
Date: Aug 23
Speaker: Nils Anders Danielsson
Abstract:
I have defined an inductiverecursive family (in Haskell terms: a fancy GADT) for a simple dependently typed language in agdaLight. I will discuss the definition, including some design choices and termination issues. If there is time I will also illustrate that it is seemingly convenient to write programs using this definition by showing a normalisation result (the proof uses normalisation by evaluation).
Exploiting Type Information to Compile Agda into Haskell, video seminar with AIST, at 9.00 in video conf. room, AVcentralen, Vhouse
Date: Jun 16
Speaker: Norio KATO
Abstract:
I will present an optimizing translator from Agda to Haskell. The translator attempts to compile Agda datatypes into their natural counterparts in Haskell so that runtime overheads will be reduced. General untyped representation is used for those types for which no such counterparts have been found. Some empirical results and present problems will be shown.
Verifying Warshall's algorithm in Agda, room 6128
Date: Jun 14
Speaker: Michael Hedberg
Abstract:
The algorithm is about finding the transitive closure of a boolean square matrix.
Rather than formalizing a mathematical model of the imperative language in which the algorithm is naturally expressed, the algorithm is "manually" transformed into a functional program.
The functional program may with some effort be shown to be equivalent to another program which is more easily seen to be correct.
The difference between the two programs lies in treatment of vector assignment.
The safe way to do X:= f(X) for vector X is to use temporary vector T: FOR i:= ... DO T[i]:= f(X)[i];FOR i:= ... DO X[i]:=T[i].
The abovementioned "effort" lies in justifying the unsafe implementation: FOR i:= ... DO X[i] := f(X)[i].
Normalization by Evaluation for MartinLöf Type Theory with One Universe
Date: Jun 7
Speaker: Peter Dybjer
Abstract:
It is a somewhat updated version of the talk I gave in Japan last month on joint work with Andreas Abel and Klaus Aehlig.
I will start with an introduction to normalization by evaluation and intuitionistic model construction. Then I will explain how to write an algorithm for normalization in Gödel System T, and how to prove it correct. Finally, I will show how this algorithm needs to be modified in order to yield an algorithm for MartinLöf type theory with one universe.
Testing properties of generic functions
Date: May 31
Speaker: Patrik Jansson
Abstract:
Generic functional programming is a paradigm for expressing generic algorithms parametrized by types. Examples of such algorithms are equality tests, traversals and pretty printers. Concrete instances can be obtained by instantiating a template algorithm with (the structure of) a datatype.
Generic functions satisfy generic properties. Since generic functions essentially consist of several functions combined in one, testing or proving properties of generic functions becomes harder.
In this talk I will show how properties of generic functions in Generic Haskell can be formulated and tested using QuickCheck. (And more interestingly, what cannot easily be formulated or tested.)
Agda II  Take One, video seminar, at 9.00 in video conf. room, AVcentralen, Vhouse
Date: May 10
Speaker: Ulf Norell
Abstract:
I will present the first version of the Agda II language and some of the motivations behind it. In particular I will talk about what is in the language:  datatypes and functions by pattern matching
 implicit arguments
 fancy module system
and what is not:  pi in set
 signatures and structures
 inductive families
and try to convey the reasons why this is so. The presentation will be accompanied by a healthy amount of simple examples illustratating the syntax of the language and how the different features can be used.
Proof Search by Lazy Instantiation of FirstOrder Terms
Date: Apr 26
Speaker: Fredrik Lindblad
Abstract:
The method that underlies the systematic construction of terms in Agsy (the proof search tool for Agda) can be described as "lazy instantiation", i.e. instantiate what you need in order to proceed with the lazy evaluation. I will examplify this by applications in automatic testing and function synthesis.
The same idea can be applied on the construction of firstorder terms, leading to a very simple, Prologlike system. I will demonstrate a compiler for a small functional language, which supports search by lazy instantiation.
A natural question is whether proof search (in Agda) is itself appropriate to formulate as a problem in such a language. This would amount to writing a typechecker and then running a search where the type but not the term is specified. I will present some ideas on the viability of representing Agsy in this way.
Interaction with a Proof Editor
Date: Apr 12
Speaker: Bengt Nordström
Abstract:
The idea is that the user of an editor for proofs (or programs, or documents) should be able to use textediting and structureediting freely. The editors alfa and half developed earlier in the department have mainly been structural editors where all parts of the proof/ program always have been typecorrect. We want to loosen the straight jacket of always being correct. (At least when it comes to proving.)
Sized (Co)Inductive Types (With Applications to Generic Programming)
Date: Apr 5
Speaker: Andreas Abel (LudwigMaximilians Universität, Munich)
Abstract:
A type system for recursive and corecursive functions over equiinductive and coinductive types is presented in which all programs are strongly normalizing. The type system supports data types of higher kind and arbitrary rank polymorphism and therefore accepts recursive functions whose termination cannot be shown with methods based on term orderings alone. (Such functions typically arise in generic programming.)
The choice of equiinductive types, instead of the more common isoinductive types, influences both reduction rules and the strong normalization proof. By embedding iso into equitypes, the latter ones are recognized as more fundamental. A model based on orthogonality is constructed where a semantical type corresponds to a set of observations, and soundness of the type system is proven.
General Recursion and CoInductive Types
Date: Mar 29
Speaker: Ana Bove
Abstract:
On one hand, we have the BoveCapretta (inductive) method to define partial and general recursive functions in type theory.
On the other hand, we have Venanzio Capretta's paper showing how one could use coinductive types to represent partiality in type theory.
Can we combine both method and define a BoveCapretta (coinductive) method which has the advantages of both previous work?
In this talk I will assume you know about the BC (inductive method) (otherwise you can get a copy of my PhD thesis, a bit more than 200 pages! :) and I will present some of the ideas in Venanzio's paper "General Recursion via Coinductive Types". While presenting Venanzio's work, I intend to show how to prove properties coinductively. Besides a whiteboard explanation, I will demonstrate the Coq proof assistant for these kind of proofs. So this talk can be thought of as a very informal and very basic tutorial on coinductive types and proofs. Be aware I have only worked with coinductive types for a short while, so I won't have many of the answers you might be looking for!
The talk will end with some words on how to combine both methods. Hopefully, this will be the topic of one of the talks at TYPES.
Generating natural language for mathematical exercises
Date: Mar 15
Speaker: Jordi Saludes (Universitat Politècnica de Catalunya (Barcelona))
Links: link
Abstract:
The main goal of the webALT project is providing a repository of calculus and linear algebra exercises for freshmen that can be automatically rendered in different languages from encoded semantics. The Grammar Framework is the tool driving the exercise editor and providing these renderings.
Certificate translation, at 10.15 in 5453
(Joint work with G. Barthe, B. Gregoire, and C. Kunz)
Date: Mar 15
Speaker: Tamara Rezk (INRIA SophiaAntipolis)
Abstract:
Program verification techniques based on programming logics and verification condition generators provide a powerful means to reason about programs. Whereas these techniques have very often been employed in the context of highlevel languages in order to benefit from their structural nature, it is often required, especially in the context of mobile code, to prove the correctness of compiled programs. Thus it is highly desirable to have a means of bringing the benefits of source code verification to code consumers.
We propose certificate translation, a mechanism that allows to transfer evidence from source programs to compiled programs. It builds upon the notion of certificate, which is used in Proof Carrying Code architectures to convey to the code consumer easily verifiable evidence that programs respect some policy. A certificate translator is an algorithm that turns certificates of source programs into certificates of compiled programs; its definition is tightly bound to the compiler used for programs, and the main difficulty in defining one stems from the optimizations performed by the compiler. In order to illustrate the feasibility of our approach, we build certificate translators for an optimizing compiler from a simple imperative language to an intermediate RTL language.
Relations in Dependent Type Theory
Date: Mar 8
Speaker: Carlos Gonzalía (Chalmers)
Abstract:
This thesis investigates how to express and reason about relational concepts and methods inside the constructive logical framework of MartinLöf's monomorphic type theory. We cover several areas where the notion of relation is central, and show how to formalize the basic concepts of each area. This formalization is carried out in a computer proof assistant for MartinLöf's type theory called Agda/Alfa, and this software allows the practical handling of the numerous technical details involved in such a task. The first area we investigate is relations and relational systems themselves. Many of the relational systems in use within computer science are based on algebras that extend Boolean algebra, and hence are unsuitable for a constructive framework. Instead we use the constructive algebra of relations provided by the categorical theory of allegories. First, we introduce the notion of an Eallegory, the appropriate abstract notion of an allegory formalizable in MartinLöf type theory. Then we set up two concrete instances: the Eallegory of Erelations, and the Eallegory of finite decidable Erelations. We investigate further properties of the Eallegories and note that only the latter satisfies the axioms of a power allegory and a Boolean allegory.
The second area is relational program construction and derivation. MartinLöf type theory provides its own approach to program construction via the identification of propositions and types, and our goal is to supplement this methodology with techniques from relational programming. Here we note that MartinLöf type theory is based on a functional notion of program, and provides a logical setting where we can reason about the connections between functional and relational notions of programs. We show some links and differences with typetheoretic program construction and derivation. We then show how recursive relations can be dealt with in type theory using the concept of relational catamorphism.
The third area is the relational database model. This data model has similarities and connections with relational algebras and allegories, but presents new problems in the way typings are handled via schemes and attributes. We set up an increasingly complex series of formalizations of the relational model, with different decidability characteristics and with respect to the way in which the scheme/attribute typing issues are handled. The final formalization, which is both the most complex and the most satisfactory, is built on an abstract finite set layer, and can be seen as an abstraction for implementations of database managers.
Abstraction and Substitution by FregeGentzen Approach, NOTE: irregular day and time: Monday, Mar 6, at 15.15, in 5453
Date: Mar 6
Speaker: Masahiko Sato (Kyoto University)
Abstract:
Frege and Gentzen used two disjoint sets of variables, namely the sets of free variables and bound variables, as the basic building blocks for constructing syntactic entities like propositions and proofs. For Frege, in particular, free variables are always tied with the notion of inference which enables us to proceed from already asserted judgments to a new judgment.
In this talk, we will follow FregeGentzen approach, and will show that substitution can be defined without appealing to the notion of alphaequivalence, and also show that we can define alphaequivalence more naturally compared to traditional approach. It is hoped that this approach is useful in practice for implementing proof assistant systems on a computer.
Proving Reducibility of Recursively Defined Constants
Date: Feb 22
Speaker: David Wahlstedt
Abstract:
I will, informally and in interaction with you, present a problem I'm currently facing.
Im working on an extension of the result presented in my Licentiate dissertation, which was to prove normalisation for a combination of a framework similar to MartinLöf's LF and dependently typed recursive patternmatching definitions, justified by the "sizechange principle for program termination" (Lee, Jones, BenAmram '01). However, the system was restricted to nonparametric data types and computation rules not taking functions as arguments, nor returning functions. The introduction of parametric data types seems to be an easy extension so far, and the important parts of the old normalisation proof are essentially unchanged. The idea is now to relax the restriction on recursive computation rules, and allow functions both in the arguments and in the result. We should also allow curried functions.
When looking at the old proof, there is no good reason it shouldn't scale up, but of course I need a better argument ;>
I have an over all structure of a proof that seems convincing, but it is difficult to get the details right, and this is crucial.
I will first try to "throw you into the core problem" in an informal way, and then (after a break ?) try to explain some technical aspects. I will not talk about sizechange termination here, since this is just a special (though quite general) case of an abstract property assumed in this part of the proof.
Implicit arguments in Agda2
Date: Feb 8
Speaker: Ulf Norell
Abstract:
I will talk about implicit arguments in Agda2. More specifically a strategy for figuring out were the implicit arguments should go.
Notation:
{x:A} > B is the hidden pi
f {x} is the explicit application of an implicit argument
? is a meta variable
\{x:A} > t is a hidden lambda (of type {x:A} > B)
\{x} > t is a domainfree hidden lambda We want to define a transformation that inserts meta variables for implicit arguments in a term. Below I will call this transformation >
Examples:
Assume id : {A:Set} > A > A
then id x > id {?} x
What about 'id'?
id > id {?}
or id > id
How about higher order hiding?
foo : ({A:Set} > A > A) > N > N
foo g n = g n
foo id 0 > foo id 0  ?
bar : {A:Set} > (A > A) > A > A
bar g n = g n
bar id 0 > bar {N} (id {N}) 0
In the meeting I will present a powerful yet elegant algorithm for this transformation.