Drafts and Publications

A Predicative Strong Normalisation Proof for a λ-calculus with Interleaving Inductive Types DVI PS
With Thorsten Altenkirch.
Types for Proofs and Programs, International Workshop, TYPES '99
Lökeberg, Sweden, June 1999. LNCS 1956. ©Springer-Verlag, 2000. We present a strong normalisation proof for a λ calculus with interleaving strictly positive inductive types λ-μ which is predicative: it uses only predicative, i.e. strictly positive inductive definitions on the metalevel. To achieve this we show that every strictly positive operator on types gives rise to an operator on saturated sets which is not only monotone but also (deterministically) set based -- a concept introduced by Peter Aczel in the context of intuitionistic set theory. We also extended this to coinductive types using greatest fixpoints of strictly monotone operators on the metalevel.

Specification and Verification of a Formal System for Structurally Recursive Functions DVI PS
Types for Proofs and Programs, International Workshop, TYPES '99
Lökeberg, Sweden, June 1999. LNCS 1956. ©Springer-Verlag, 2000. We introduce a type theoretic programming language based on lambda calculus with coproducts, products and inductive types that allows definition of recursive functions in the way that is common in most functional programming languages. We present a formal system that checks whether such a definition is structural recursive and give a elaborate soundness proof for this system. Thus we ensure that all functions passing this check terminate on all inputs. For the moment we restrict ourselves to non-mutual recursive functions.

A Predicative Analysis of Structural Recursion DVI PS
Joint work with Thorsten Altenkirch. Submitted to JFP (1999)
We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the definition of recursive terms. We present the implementation ("foetus") of a syntactical check that ensures that all such terms are structurally recursive, i.e. recursive calls appear only with arguments structurally smaller than the input parameters of considered terms. To ensure the correctness of the termination checker, we show that all structurally recursive terms are normalizing with respect to a given operational semantics. To this end, we define a semantics on all types and a structural ordering on the values in this semantics and prove that all values are accessible with regard to this ordering. Finally we point out how to do this proof predicatively using set based operators.

A Semantic Analysis of Structural Recursion DVI PS
Diploma Thesis (1999)
We consider a type theoretic language with lambda abstraction, disjoint unions, pairs and recursive terms and show that all structurally recursive functions terminate, i.e. functions, that contain recursive calls only with a structurally smaller argument. Therefore we define a semantics [| T |] over all types T and show that it is wellfounded w.r.t. the structural ordering on the values (normal forms of our terms). Then by wellfounded induction we can easily infer termination of a recursive function at all inputs in [| T |] from termination at all smaller inputs. Later we extend our solution from strictly positive types to positive types and mutual recursive functions.
Extended abstract HTML DVI PS
Errata HTML DVI PS

foetus - Termination Checker for Simple Functional Programs HTML DVI PS
Implementation and Documentation (1998)
We briefly introduce a simple functional language foetus (lambda calculus with tupels, constructors and pattern matching) on which we have implemented a termination checker. This checker tries to find a well-founded structural order on the parameters on the given function. The components of the check algorithm are: function call extraction out of the program text, call graph completion and finding a lexical order for the function parameters. The HTML version of this paper contains many ready-to-run Web-based examples.

Division nach Beame, Cook & Hoover HTML DVI PS
Seminar Talk (1996)
Diese Seminararbeit behandelt ausführlich den Beweis, dass Ganzzahl-Division in der Komplexitätsklasse NC enthalten ist, d.h. dass eine Klasse von Schaltkreisen existiert, die x div y in zu der Länge der Eingaben x und y linearer Zeit berechnet. Ermöglicht wird es durch Inversenbildung von y mittels einer geometrischen Reihe, welche mit Hilfe von diskreten Logarithmen in NC berechnet werden kann.
Keywords: complexity theory, division circuit, discrete logarithm, iterated product

Notes

A Coinductive Formulation of the "Coinduction Theorem" by Michael and Appel DVI PS
Mini-tutorial of Coinduction with Application (2000)
We show how the definition of safety in Michael's and Appel's CADE-17 article can be restated coinductively

Pattern Matching vs. Elimination Rules DVI PS
A Case Study in LEGO (1999)
We define an ordering and show the admissibility of one additional rule first by pattern matching and then in the elimination style. We apply the translation of pattern matching definitions into recursive schemes given by Eduardo Gimenez.
Keywords: pattern matching, elimination, admissible rule, LEGO

[ Home | CV | Publications | Projects ]
[ Personal page | Home@LMU,Munich ]

abel@cs.cmu.edu
http://www.cs.cmu.edu/~abel