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.
©SpringerVerlag,
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.
©SpringerVerlag,
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 nonmutual 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 wellfounded 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 readytorun
Webbased examples.
Division nach Beame, Cook & Hoover
HTML
DVI
PS
Seminar Talk (1996)
Diese Seminararbeit behandelt ausführlich den Beweis, dass
GanzzahlDivision 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
Minitutorial of Coinduction with Application (2000)
We show how the definition of safety in Michael's and Appel's
CADE17 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
