Andreas Abel, Thorsten Altenkirch
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...
Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory (2009)
Andreas Abel, Thierry Coqu, Peter Dybjer
Abstract. Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of...
Type Structures and Normalization by Evaluation for System F ω (2009)
We present the first verified normalization-by-evaluation algorithm for System F ω, the simplest impredicative type theory with computation on the type level. Types appear in three shapes: As...
In the simply-typed lambda-calculus, a hereditary substitution replaces a free variable in a normal form r by another normal form s of type a, removing freshly created redexes on the y. It can be de...
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory (2009)
Abstract. An algebraic presentation of Martin-Löf’s intuitionistic type theory is given which is based on the notion of a category with families with extra structure. We then present a...
A Partial Type Checking Algorithm for Type: Type (2009)
Andreas Abel, Thorsten Altenkirch
We analyze a partial type checking algorithm for the inconsistent domain-free pure type system Type:Type (λ∗). We show that the algorithm is sound and partially complete using a coinductive...
Strong normalization and equi-(co)inductive types (2009)
Abstract. A type system for the lambda-calculus enriched with recursive and corecursive functions over equi-inductive and-coinductive types is presented in which all well-typed programs are strongly...
Constructing Type-Safe Operators for Software Composition ⋆ (2009)
Axel Rauschmayer, Andreas Abel, Martin Wirsing
Abstract. Grey-box software composition appears in many areas of software engineering: Mixin layers, aspects and traits are just a few examples and even regular inheritance can be viewed as...
Semi-continuous Sized Types and Termination (2008)
Some type-based approaches to termination use sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is visible...
LFM 2004 Preliminary Version Weak Normalization for the Simply-Typed Lambda-Calculus in Twelf (2008)
Weak normalization for the simply-typed λ-calculus is proven in Twelf, an implementation of the Edinburgh Logical Framework. Since due to proof-theoretical restrictions Twelf Tait’s computability...
Carsten Schürmann (chair, Thierry Coquand, Dale Miller Inria, Carsten Schürmann, Andreas Abel, Jason Reed
Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their...
Abstract. The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces Λ + µ, a lambda-calculus with recursion, inductive types,...
Semi-continuous sized types and termination (2008)
Abstract. A type-based approach to termination uses sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is...
Mixed Inductive/Coinductive Types and Strong Normalization (2008)
Abstract. We introduce the concept of guarded saturated sets, saturated sets of strongly normalizing terms closed under folding of corecursive functions. Using this tool, we can model equi-inductive...
Constructing Type-Safe Operators for Software Composition ⋆ (2008)
Axel Rauschmayer, Andreas Abel, Martin Wirsing
Abstract. Grey-box software composition appears in many areas of software engineering: Mixin layers, aspects and traits are just a few examples and even regular inheritance can be viewed as...
Primitive Recursion for Rank-2 Inductive Types (2008)
Recently, higher-rank datatypes have drawn interest in the functional programming community [Oka99,Oka96,Hin01]. Rank-2 non-regular types, so-called nested datatypes, have been investigated in the...
and Reasoning about Programs—Mechanical verification (2008)
Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell
Proof assistants based on dependent type theory are closely related to functional programming languages, and so it is tempting to use them to prove the correctness of functional programs. In this...
Abstract LFM 2004 Preliminary Version Normalization for the Simply-Typed (2008)
Normalization for the simply-typed λ-calculus is proven in Twelf, an implementation of the Edinburgh Logical Framework. Since due to proof-theoretical restrictions Twelf Tait’s computability...
Semi-continuous sized types and termination (2008)
Abstract. A type-based approach to termination uses sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is...
Termination and Productivity Checking with Continuous Types (2008)
Abstract. We analyze the interpretation of inductive and coinductive types as sets of strongly normalizing terms and isolate classes of types with certain continuity properties. Our result enables us...
Semi-continuous sized types and termination (2008)
Abstract. A type-based approach to termination uses sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is...
Abstract. Giménez ’ type system for structural recursion in the Calculus of Constructions is adapted to typed functional programming. As core language, the λ-calculus with inductive types,...
Gimenez' type system for structural recursion in the Calculus of Constructions is adapted to typed functional programming. As core language, the #-calculus with inductive types, subtyping and...
Verifying a semantic βη-conversion test for Martin-Löf type theory (2008)
Andreas Abel, Thierry Coqu, Peter Dybjer
Abstract. Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of...
Weak βη-normalization and normalization by evaluation for System F (2008)
Abstract. A general version of the fundamental theorem for System F is presented which can be instantiated to obtain proofs of weak β- and βη-normalization and normalization by evaluation. 1...
0-7803-4455-3/98/$10.00 (c) 1998 IEEE STATISTICAL ANALYSIS OF CHAOTIC COMMUNICATION SCHEMES (2007)
Andreas Abel, Marco Götz, Wolfgang Schwarz
abel,goetz,schwarz¡ On the base of the estimator variance analysis we present a classification for a number digital chaos communication schemes and conventional spread spectrum techniques, which...
DESIGN OF INFINITE CHAOTIC POLYPHASE SEQUENCES WITH PERFECT CORRELATION PROPERTIES (2007)
In this paper we consider chaotic discrete-time systems which generate polyphase sequences. First we give the definition of infinite polyphase sequences with perfect correlation properties. Then a...
Andreas Abel, Wolfgang Schwarz
Abstract — The paper describes the application of the Viterbi algorithm in the implmentation of a maximum likelihood receiver in a chaos communication scheme. The Viterbi decoder is constructed...
A Nonlinear Bayesian Filter for Chaotic Piecewise Linear Maps (2007)
Marco Götz, Andreas Abel, Wolfgang Schwarz
In this paper we derive the Bayesian filter for chaotic signals generated by piecewise linear maps. We give the basic signal model containing an additive Gaussian noise and solve the Bayesian state...
Generation of Broadband Noise-Like Signals for Measurement and Location Purposes (2007)
Andreas Abel, Andreas Bauer, Thomas Falk, Marco Götz, Kristina Kelber, Torsten Kilias, ...
This paper considers the generation of chaotic signals and selected application fields with emphasis to measurements. Table 1.1 summarises the features for the application of chaotic systems and...
Set-based Operators and Fixed-Points by Support (2007)
Andreas Abel, U Val, Abel Altenkirch Pierce
In Abel and Altenkirch's article A Predicative Analysis of Structural Recursion [AA02] one nds on page 34 a denition of the semantics [[]] of a strictly positive inductive type . This denition...
I. MULTI-USER CHANNELS Objectives and Resources (2007)
Andreas Abel, Andreas Bauer, Kristina Kelber, Wolfgang Schwarz
Abstract This paper gives a tutorial-like intro-duction to the use of chaotic codes in code devision multiple access (CDMA) systems. First, general principles of sharing resources between different...
Andreas Abel, Thorsten Altenkirch
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...
Andreas Abel, Thorsten Altenkirch
Abstract. We present a new strong normalisation proof for a-calculus with interleaving strictly positive inductive types which avoids the use of impredicative reasoning, i.e., the theorem of...
Proof terms for the implicational fragment of classical logic in natural deduction style Raw terms: M:: = x j x:M j MM j a:N (Unnamed) terms N:: = [a]M Named terms Typing rules resp. proof rules:
A Third-Order Representation of the-Calculus (2007)
Abstract. Higher-order logical frameworks provide a powerful technology to reason about object languages with binders. This will be demonstrated for the case of the-calculus with two different...
Andreas Abel, Acknowledgements Ralph Matthes, Frank Pfenning, Brigitte Pientka
Parigot's -Calculus Proof terms for the implicational fragment of classical logic in natural deduction style Raw terms: M:: = x j x:M j MM j a:N (Unnamed) terms N:: = [a]M Named terms Typing...
Andreas Abel, Thorsten Altenkirch
Abstract. We present a new strong normalisation proof for a-calculus with interleaving strictly positive inductive types which avoids the use of impredicative reasoning, i.e., the theorem of...
Human-Readable Machine-Veriable Proofs for Teaching Constructive Logic (2007)
Abstract. A linear syntax for natural deduction proofs in rst-order intuitionistic logic is presented, which has been an eective tool for teaching logic. The proof checking algorithm is also given,...
Constructing Type-Safe Operators for (2007)
Software Composition Axel, Axel Rauschmayer, Andreas Abel, Martin Wirsing
Grey-box software composition appears in many areas of software engineering: Mixin layers, aspects and traits are just a few examples and even regular inheritance can be viewed as composition....
Primitive Recursion for Rank-2 Inductive Types (2007)
Recently, higher-rank datatypes have drawn interest in the functional programming community [Oka99,Oka96,Hin01]. Rank-2 non-regular types, so-called nested datatypes, have been investigated in the...
Normalization by evaluation for Martin-Löf type theory with one universe (2007)
Andreas Abel, Klaus Aehlig, Peter Dybjer, Abel Aehlig Dybjer
Replace this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be
Normalization by evaluation for Martin-Löf type theory with one universe (2007)
The decidability of equality is proved for Martin-Löf type theory with a universe á la Russell and typed betaeta-equality judgements. A corollary of this result is that the constructor for...
Normalization by evaluation for Martin-Löf type theory with one universe (2007)
Andreas Abel, Klaus Aehlig, Peter Dybjer, Abel Aehlig Dybjer
Replace this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be
My Interest on Normalization in Weak Metatheories (2007)
Weak systems can be shown consistent in (almost as) weak meta-theories. Normalization implies usually consistency. Tait’s semantical normalization proof for the simply-typed λ-calculus (STL) is...
Type-based termination of generic programs (2007)
Instances of a polytypic or generic program for a concrete recursive type often exhibit a recursion scheme that is derived from the recursion scheme of the instantiation type. In practice, the...
Type-based termination of generic programs (2007)
Instances of a polytypic or generic program for a concrete recursive type often exhibit a recursion scheme that is derived from the recursion scheme of the instantiation type. In practice, the...
Syntactical Strong Normalization for Intersection Types with Term Rewriting Rules (2007)
We investigate the intersection type system of Coquand and Spiwack with rewrite rules and natural numbers and give an elementary proof of strong normalization which can be formalized in a weak...
Normalization by evaluation for Martin-Löf type theory with one universe (2007)
The decidability of equality is proved for Martin-Löf type theory with a universe á la Russell and typed betaeta-equality judgements. A corollary of this result is that the constructor for...
Syntactical Strong Normalization for Intersection Types with Term Rewriting Rules (2007)
We investigate the intersection type system of Coquand and Spiwack with rewrite rules and natural numbers and give an elementary proof of strong normalization which can be formalized in a weak...
Ludwig-Maximilians-University Munich (2007)
Research: normalization proofs in Twelf. Twelf: higher-order abstract syntax. Comfortable variable handling, but no recursive functions. Only Π2 statements (∀x∃yA).
Local Organization: Event4 Event Management Preface (2007)
Brigitte Pientka, Carsten Schürmann, Andreas Abel, Brigitte Pientka, Brigitte Pientka
Frameworks and Meta-Languages ” and the MERλIN workshop series on “MEchanized Reasoning about Languages with variable BInding”. Logical frameworks and meta-languages form a common substrate...
Implementing a normalizer using sized heterogeneous types (2006)
In the simply-typed lambda-calculus, a hereditary substitution replaces a free variable in a normal form r by another normal form s of type a, removing freshly created redexes on the fly. It can be...
Implementing a normalizer using sized heterogeneous types (2006)
In the simply-typed lambda-calculus, a hereditary substitution replaces a free variable in a normal form r by another normal form s of type a, removing freshly created redexes on the fly. It can be...
Verifying Haskell programs using constructive type theory (2005)
Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell
Abstract Proof assistants based on dependent type theory are closely relatedto functional programming languages, and so it is tempting to use them to prove the correctness of functional programs. In...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a first-order theorem prover. Its main purpose is to keep track...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a firstorder theorem prover. Its main purpose is to keep track of...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a firstorder theorem prover. Its main purpose is to keep track of...
Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs (2005)
Abstract. An untyped algorithm to test βη-equality for Martin-Löf’s Logical Framework with strong Σ-types is presented and proven complete using a model of partial equivalence relations between...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a firstorder theorem prover. Its main purpose is to keep track of...
Verifying Haskell programs using constructive type theory (2005)
Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell
Abstract Proof assistants based on dependent type theory are closely relatedto functional programming languages, and so it is tempting to use them to prove the correctness of functional programs. In...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a first-order theorem prover. Its main purpose is to keep track...
Type Theory with First-Order Data Types and Size-Change Termination. Licentiate thesis (2004)
David Wahlstedt, David Wahlstedt, C David Wahlstedt, Michael Hedberg, Andreas Abel, Björn Bjurling, ...
We prove normalization for a dependently typed lambda-calculus extended with first-order data types and computation schemata for first-order size-change terminating recursive functions. Size-change...
Weak Normalization for the Simply-Typed Lambda-Calculus in Twelf (Extended Abstract) (2004)
Andreas Abel Department of Computer Science, Chalmers University of Technology Rannvagen 6, SWE-41296 Goteborg, Sweden Abstract. Weak normalization for the simply-typed -calculus is proven in...
Iteration and Coiteration Schemes for Higher-Order and Nested Datatypes (2004)
Andreas Abel, Ralph Matthes, Tarmo Uustalu
This article studies the implementation of inductive and coinductive constructors of higher kinds (higher-order nested datatypes) in typed term rewriting, with emphasis on the choice of the iteration...
Fixed points of type constructors and primitive recursion (2004)
Our contribution to CSL 04 [AM04] contains a little error, which is easily corrected by 2 elementary editing steps (replacing one character and deleting another). Definition of wellformed contexts...
Fixed points of type constructors and primitive recursion (2004)
Abstract. For nested or heterogeneous datatypes, terminating recursion schemes considered so far have been instances of iteration, excluding efficient definitions of fixed-point unfolding. Two...
Weak normalization for the simply-typed lambda-calculus in Twelf (2004)
Abstract. Weak normalization for the simply-typed λ-calculus is proven in Twelf, an implementation of the Edinburgh Logical Framework. Since due to proof-theoretical restrictions Twelf Tait’s...
Fixed points of type constructors and primitive recursion (2004)
Abstract. For nested or heterogeneous datatypes, terminating recursion schemes considered so far have been instances of iteration, excluding efficient definitions of fixed-point unfolding. Two...
Fixed Points of Type Operators and Primitive Recursion (2004)
Abstract. For nested or heterogeneous datatypes, terminating recursion schemes considered so far have been instances of iteration, excluding efficient definitions of fixed-point unfolding. Two...
Fixed points of type constructors and primitive recursion (2004)
Abstract. For nested or heterogeneous datatypes, terminating recursion schemes considered so far have been instances of iteration, excluding efficient definitions of fixed-point unfolding. Two...
[AA02] one finds on page 34 a definition of the semantics [[σ]] of a strictly positive inductive type σ. This definition (5.1) is itself a strictly-positive inductive definition on the meta-level....
Fachkonzept für die Implementierung privater Währungen im Internet / (2003)
Zugl.: Magdeburg, Universiẗat, Diss., 2003.
Generalized iteration and coiteration for higher-order nested datatypes (2003)
Andreas Abel, Ralph Matthes, Tarmo Uustalu, Programmes Et Systèmes
Abstract. We solve the problem of extending Bird and Paterson’s generalized folds for nested datatypes and its dual to inductive and coinductive constructors of arbitrarily high ranks by...
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes (2003)
Andreas Abel, Ralph Matthes, Tarmo Uustalu, Programmes Et Systemes
We solve the problem of extending Bird and Paterson's generalized folds for nested datatypes and its dual to inductive and coinductive constructors of arbitrarily high ranks by appropriately...
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes (2003)
Andreas Abel, Ralph Matthes, Tarmo Uustalu, Programmes Et Systemes
We solve the problem of de ning generalized iteration (generalized in the direction of generalized folds by Bird and Paterson) and its dual for inductive and coinductive constructors (nested...
This document gives a Haskell implementations of the examples in the article Iteration and Coiteration for Higher-Order Nested Datatypes by Abel and Matthes [AM03]. The programs make essential use of...
Co-)iteration for higher-order nested datatypes (2003)
Abstract. The problem of defining iteration for higher-order nested datatypes of arbitrary (finite) rank is solved within the framework of System F ω of higher-order parametric polymorphism. The...
Generalized iteration and coiteration for higher-order nested datatypes (2003)
Andreas Abel, Ralph Matthes, Tarmo Uustalu, Programmes Et Systèmes
Abstract. We solve the problem of extending Bird and Paterson’s generalized folds for nested datatypes and its dual to inductive and coinductive constructors of arbitrarily high ranks by...
Generalized iteration and coiteration for higher-order nested datatypes (2003)
Andreas Abel, Ralph Matthes, Tarmo Uustalu, Programmes Et Systèmes
Abstract. We solve the problem of defining generalized iteration (generalized in the direction of generalized folds by Bird and Paterson) and its dual for inductive and coinductive constructors...
Generalized Iteration and CoIteration for Higher-Order Nested Datatypes (2003)
Andreas Abel, Ralph Matthes, Tarmo Uustalu
The problem of de ning iteration for higher-order nested datatypes of arbitrary ( nite) rank is solved within the framework of System F of higher-order parametric polymorphism. The proposed solution...
Haskell Examples for Iteration and Coiteration on Higher-Order Datatypes (2003)
Andreas Abel, Coinductive Types
This document gives a Haskell implementation of the examples in the article Iteration and Coiteration for Higher-Order Nested Datatypes by Abel and Matthes [AM03]. The programs make essential use of...
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes (2003)
Andreas Abel, Ralph Matthes, Tarmo Uustalu, Programmes Et Systemes
We solve the problem of extending Bird and Paterson's generalized folds for nested datatypes and its dual to inductive and coinductive constructors of arbitrarily high ranks by appropriately...
Termination and Productivity Checking with Continuous Types (2003)
We analyze the interpretation of inductive and coinductive types as sets of strongly normalizing terms and isolate classes of types with certain continuity properties. Our result enables us to relax...
(Co-)Iteration for Higher-Order Nested Datatypes (2003)
The problem of de ning iteration for higher-order nested datatypes of arbitrary ( nite) rank is solved within the framework of system F of higher-order parametric polymorphism. The proposed solution...
Slide 6 Totality of Recursive Definitions (2002)
2. Totality proof (supported by tactics) • Bove (proof of accessibility) • Bertot (proof of well-definedness) 3. Syntactic (fully automatic) • By static analysis of code (Coquand 1992 [3],...
Andreas Abel, Berg En Dal, Miculan (ordered Uniformities, Inductive Datatypes
List(Nat) insert = a: x g Y !List(Nat) Nil ) Cons(a; Nil) ) ) if a x then Cons(a; Cons(x; xs Y List(Nat) )) else Cons(x; g xs Coercion Y F may be used : Stronger than iteration. 4 Mendler-style...
Human-readable machine-verifiable proofs for teaching constructive logic (2001)
Abstract. A linear syntax for natural deduction proofs in first-order intuitionistic logic is presented, which has been an effective tool for teaching logic. The proof checking algorithm is also...
Human-readable machine-verifiable proofs for teaching constructive logic (2001)
Abstract. A linear syntax for natural deduction proofs in first-order intuitionistic logic is presented, which has been an effective tool for teaching logic. The proof checking algorithm is also...
A third-order representation of the λµ-Calculus (2001)
Abstract. Higher-order logical frameworks provide a powerful technology to reason about object languages with binders. This will be demonstrated for the case of the λµ-calculus with two different...
Human-readable machine-verifiable proofs for teaching constructive logic (2001)
Abstract. A linear syntax for natural deduction proofs in first-order intuitionistic logic is presented, which has been an effective tool for teaching logic. The proof checking algorithm is also...
Introduction 2. Recursion plus Examples 3. Corecursion plus Examples 4. Continuous Types 5. Strong Normalization 6. Further and Related Work Work supported by: PhD Programme Logic in Computer...
Specification and verification of a formal system for structurally recursive functions (2000)
Abstract. A type theoretic programming language is introduced that is based on lambda calculus with coproducts, products and inductive types, and additionally allows the definition of recursive...
Specification and verification of a formal system for structurally recursive functions (2000)
Abstract. A type theoretic programming language is introduced that is based on lambda calculus with coproducts, products and inductive types, and additionally allows the definition of recursive...
Termination of Mutually Recursive Functions (2000)
Introduction 2. The foetus Project 3. Mutually Recursive Functions with One Argument 4. Mutually Recursive Functions with Several Arguments Recursion over Inductive Types Functional programming...
A predicative strong normalisation proof for a λ-calculus with interleaving inductive types (2000)
Andreas Abel, Thorsten Altenkirch
Abstract. We present a new strong normalisation proof for a λ-calculus with interleaving strictly positive inductive types λ µ which avoids the use of impredicative reasoning, i.e., the theorem of...
A predicative strong normalisation proof for a λ-calculus with interleaving inductive types (2000)
found the following errors: p. 28 Definition of weak head reduction. The correct definition is: p. 28 Lemma 1. Proposition 3 t ✄β u t ✄whd u t ✄whd t ′ t ✄whd u
A predicative analysis of structural recursion (1999)
Andreas Abel, Thorsten Altenkirch
Abstract. We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the de nition of recursive terms. We present the...
A predicative strong normalisation proof for a λ-calculus with interleaving inductive types (1999)
Andreas Abel, Thorsten Altenkirch
We present a new strong normalisation proof for a λ-calculus with interleaving strictly positive inductive types λ^µ which avoids the use of impredicative reasoning, i.e., the theorem of...
A Predicative Analysis of Structural Recursion (1999)
Andreas Abel, Thorsten Altenkirch
. We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the denition of recursive terms. We present the implementation...
A predicative strong normalisation proof for a λ-calculus with interleaving inductive types (1999)
Andreas Abel, Thorsten Altenkirch
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...
Specification and Verification of a Formal System for Structurally Recursive Functions (1999)
. We introduce a type theoretic programming language based on lambda calculus with coproducts, products and inductive types that allows denition of recursive functions in the way that is common in...
A Semantical Analysis of Structural Recursion (1999)
Andreas Abel, Thorsten Altenkirch
dering is wellfounded at each type. A general soundness theorem allows us to conclude that each term accepted by the foetus system actually terminates. Our approach is related to the work by Telford...
A predicative analysis of structural recursion (1999)
Andreas Abel, Thorsten Altenkirch
We are developing a system (MuTTI- Munich Type Theory Implementation) with dependent types which can be used for the development of provably correct programs in Type Theory. Inspired by Coquand’s...
Termination Checking with Types (1999)
The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces , a lambda-calculus with recursion, inductive types, subtyping and...
An analysis method for the performance comparison of communication systems (1998)
Andreas Abel, Marco Götz, Wolfgang Schwarz
Information This paper demonstrates the application of cumulant equations to the analysis of non-recursive systems with polynomial characteristics, as they are often found in the baseband equivalents...
DCSK And DPSK - What Makes Them Different? (1998)
Andreas Abel, Marco Götz, Wolfgang Schwarz
In this paper we compare the chaotic Differential Chaos Shift Keying (DPSK) communication scheme with the conventional Differential Phase Shift Keying (DPSK). The two methods are similar in both,...
An Analysis Method for the Performance Comparison of Communication Systems (1998)
Andreas Abel, Marco Götz, Wolfgang Schwarz
This paper demonstrates the application of cumulant equations to the analysis of non-recursive systems with polynomial characteristics, as they are often found in the baseband equivalents of...
foetus – Termination Checker for Simple Functional Programs (1998)
We introduce a simple functional language foetus (lambda calculus with tuples, constructors and pattern matching) supplied with a termination checker. This checker tries to find a well-founded...
We introduce a simple functional language foetus (lambda calculus with tuples, constructors and pattern matching) supplied with a termination checker. This checker tries to find a well-founded...
Correlation Properties Of Signals Generated By Nonlinear AR Filter Structures (1997)
Kristina Kelber, Andreas Abel, Wolfgang Schwarz
In this paper correlation properties of signals generated by n-dimensional nonlinear AR-filter structures are considered. For continuous-value signals y(k) 2 I = [\Gamma1; 1), which possess the n-...
Chaotic Codes For Cdma Applications (1997)
Andreas Abel, Andreas Bauer, Kristina Kelber, Wolfgang Schwarz
This paper gives a tutorial-like introduction to the use of chaotic codes in code devision multiple access (CDMA) systems. First, general principles of sharing resources between different user pairs,...
What is the Use of Frobenius-Perron Operator for Chaotic Signal Processing? (1997)
Marco Götz, Andreas Abel, Wolfgang Schwarz
In this paper we demonstrate the application of the Frobenius-Perron operator to the statistical analysis of chaotic systems. The Frobenius-Perron operator is the main analysis tool whenever...
safety for a transition relation 7! on the set of machine states S as follows: