Ralph Matthes

artykuł

Decidability of Several Concepts of Finiteness for Simple Types

José Espírito Santo, Ralph Matthes, Luís Pinto

Fundamenta Informaticae > 2019 > Vol. 170, nr 1-3 > 111--138

If we consider as “member” of a simple type the outcome of any successful (possibly infinite) run of bottom-up proof search that starts from the type, then several concepts of “finiteness” for simple types are possible: the finiteness of the search space, the finiteness of any member, or the finiteness of the number of finite members (in other words, the inhabitants). In this paper we show that these...

artykuł

From Signatures to Monads in UniMath

Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

Journal of Automated Reasoning > 2019 > 63 > 2 > 285-318

The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept as small as possible in order to ease verification of it—in particular, general inductive types are not part of the system. In this work, we partially...

rozdział

Verification of the Schorr-Waite Algorithm – From Trees to Graphs

Mathieu Giorgino, Martin Strecker, Ralph Matthes, Marc Pantel

Lecture Notes in Computer Science > Logic-Based Program Synthesis and Transformation > 67-83

This article proposes a method for proving the correctness of graph algorithms by manipulating their spanning trees enriched with additional references. We illustrate this concept with a proof of the correctness of a (pseudo-)imperative version of the Schorr-Waite algorithm by refinement of a functional one working on trees. It is composed of two orthogonal steps of refinement – functional to imperative...

rozdział

Verification of the Redecoration Algorithm for Triangular Matrices

Ralph Matthes, Martin Strecker

Lecture Notes in Computer Science > Types for Proofs and Programs > 125-141

Triangular matrices with a dedicated type for the diagonal elements can be profitably represented by a nested datatype, i.e., a heterogeneous family of inductive datatypes. These families are fully supported since the version 8.1 of the Coq theorem proving environment, released in 2007. Redecoration of triangular matrices has a succinct implementation in this representation, thus giving the challenge...

rozdział

Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening

Ralph Matthes

Lecture Notes in Computer Science > Mathematics of Program Construction > 220-242

Nested datatypes are families of datatypes that are indexed over all types such that the constructors may relate different family members. Moreover, the argument types of the constructors refer to indices given by expressions where the family name may occur. Especially in this case of true nesting, there is no direct support by theorem provers to guarantee termination of functions that traverse these...

rozdział

Standardization and Confluence for a Lambda Calculus with Generalized Applications

Felix Joachimski, Ralph Matthes

Lecture Notes in Computer Science > Rewriting Techniques and Applications > Regular Papers > 141-155

As a minimal environment for the study of permutative reductions an extension ΛJ of the untyped λ-calculus is considered. In this non-terminating system with non-trivial critical pairs, confluence is established by studying triangle properties that allow to treat permutative reductions modularly and could be extended to more complex term systems with permutations. Standardization is shown by means...

rozdział

Monotone Inductive and Coinductive Constructors of Rank 2

Ralph Matthes

Lecture Notes in Computer Science > Computer Science Logic > Constructive Theory of Types > 600-614

A generalization of positive inductive and coinductive types to monotone inductive and coinductive constructors of rank 1 and rank 2 is described. The motivation is taken from initial algebras and final coalgebras in a functor category and the Curry-Howard-correspondence. The definition of the system as a λ-calculus requires an appropriate definition of monotonicity to overcome subtle problems, most...

rozdział

Generalized Iteration and Coiteration for Higher-Order Nested Datatypes

Andreas Abel, Ralph Matthes, Tarmo Uustalu

Lecture Notes in Computer Science > Foundations of Software Science and Computation Structures > Contributed Papers > 54-69

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 generalizing Mendler-style (co)iteration.Characteristically to Mendler-style schemes of disciplined (co)recursion,the schemes we propose do not rest on notions like positivity or monotonicity of a constructor...

rozdział

Recursion on Nested Datatypes in Dependent Type Theory

Ralph Matthes

Lecture Notes in Computer Science > Logic and Theory of Algorithms > 431-446

Nested datatypes are families of datatypes that are indexed over all types and where the datatype constructors relate different members of the family. This may be used to represent variable binding or to maintain certain invariants through typing. In dependent type theory, a major concern is the termination of all expressible programs, so that types that depend on object terms can still be...

rozdział

(Co-)Iteration for Higher-Order Nested Datatypes

Andreas Abel, Ralph Matthes

Lecture Notes in Computer Science > Types for Proofs and Programs > 1-20

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 proposed solution heavily relies on a general notion of monotonicity as opposed to a syntactic criterion on the shape of the type constructors such as positivity or even being polynomial. Its...

rozdział

Fixed Points of Type Constructors and Primitive Recursion

Andreas Abel, Ralph Matthes

Lecture Notes in Computer Science > Computer Science Logic > Regular Papers > 190-204

For nested or heterogeneous datatypes, terminating recursion schemes considered so far have been instances of iteration, excluding efficient definitions of fixed-point unfolding. Two solutions of this problem are proposed: The first one is a system with equi-recursive non-strictly positive type constructors of arbitrary finite kinds, where fixed-point unfolding is computationally invisible due to...

rozdział

Interpolation for Natural Deduction with Generalized Eliminations

Ralph Matthes

Lecture Notes in Computer Science > Proof Theory in Computer Science > 153-169

A modification of simply-typed λ-calculus by generalized elimination rules in the style of von Plato is presented. Its characteristic feature are permutative conversions also for function types and product types. After the addition of certain extensional reduction rules, an interpolation theorem (à la Lyndon) is proven which is also aware of the terms (a. k. a. the proofs via the Curry-Howard-isomorphism)...

rozdział

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

José Espírito Santo, Ralph Matthes, Luís Pinto

Lecture Notes in Computer Science > Typed Lambda Calculi and Applications > 133-147

The intuitionistic fragment of the call-by-name version of Curien and Herbelin’s ${{\overline{\lambda}} \mu \tilde{\mu}}$ -calculus is isolated and proved strongly normalising by means of an embedding into the simply-typed λ-calculus. Our embedding is a continuation-and-garbage-passing style translation, the inspiring idea coming from Ikeda and Nakazawa’s translation of Parigot’s λμ-calculus. The...

rozdział

Monadic Translation of Intuitionistic Sequent Calculus

José Espírito Santo, Ralph Matthes, Luís Pinto

Lecture Notes in Computer Science > Types for Proofs and Programs > 100-116

This paper proposes and analyses a monadic translation of an intuitionistic sequent calculus. The source of the translation is a typed λ-calculus previously introduced by the authors, corresponding to the intuitionistic fragment of the call-by-name variant of $\overline{\lambda}\mu\tilde{\mu}$ of Curien and Herbelin, and the target is a variant of Moggi’s monadic meta-language, where the rewrite...

rozdział

Parigot’s Second Order λμ-Calculus and Inductive Types

Ralph Matthes

Lecture Notes in Computer Science > Typed Lambda Calculi and Applications > Contributed Papers > 329-343

A new proof of strong normalization of Parigot’s (second order) λμ-calculus is given by a reduction-preserving embedding into system F (second order polymorphic λ-calculus). The main idea is to use the least stable supertype for any type. These non-strictly positive inductive types and their associated iteration principle are available in system F, and allow to give a translation vaguely related to...

rozdział

Monotone Fixed-Point Types and Strong Normalization

Ralph Matthes

Lecture Notes in Computer Science > Computer Science Logic > Contributed Papers > 298-312

Several systems of fixed-point types (also called retract types or recursive types with explicit isomorphisms) extending system F are considered. The seemingly strongest systems have monotonicity witnesses and use them in the definition of beta reduction for those types. A more naïve approach leads to non-normalizing terms. All the other systems are strongly normalizing because they embed in a reduction-preserving...

rozdział

A Datastructure for Iterated Powers

Ralph Matthes

Lecture Notes in Computer Science > Mathematics of Program Construction > Contributed Papers > 299-315

Bushes are considered as the first example of a truly nested datatype, i. e., a family of datatypes indexed over all types where a constructor argument not only calls this family with a changing index but even with an index that involves the family itself. For the time being, no induction principles for these datatypes are known. However, the author has introduced with Abel and Uustalu (TCS 333(1–2),...

artykuł

Map fusion for nested datatypes in intensional type theory

Ralph Matthes

Science of Computer Programming > 2011 > 76 > 3 > 204-224

A definitional extension LNGMIt of the Calculus of Inductive Constructions (CIC), that underlies the proof assistant Coq, is presented that allows also to program with nested datatypes that are not legal datatype definitions of CIC since they are “truly nested”. LNGMIt ensures termination of recursively defined functions that follow iteration schemes in the style of N. Mendler. Characteristically...

artykuł

Non-strictly positive fixed points for classical natural deduction

Ralph Matthes

Annals of Pure and Applied Logic > 2005 > 133 > 1-3 > 205-230

Termination for classical natural deduction is difficult in the presence of commuting/permutative conversions for disjunction. An approach based on reducibility candidates is presented that uses non-strictly positive inductive definitions.It covers second-order universal quantification and also the extension of the logic with fixed points of non-strictly positive operators, which appears to be a new...

artykuł

Iteration and coiteration schemes for higher-order and nested datatypes

Andreas Abel, Ralph Matthes, Tarmo Uustalu

Theoretical Computer Science > 2005 > 333 > 1-2 > 3-66

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 and coiteration constructions to support as primitive. We propose and compare several well-behaved extensions of System Fω with some form of iteration and coiteration uniform in all kinds. In what we...

INFONA - portal komunikacji naukowej

Wyniki wyszukiwania dla: Ralph Matthes

Decidability of Several Concepts of Finiteness for Simple Types

From Signatures to Monads in UniMath

Verification of the Schorr-Waite Algorithm – From Trees to Graphs

Verification of the Redecoration Algorithm for Triangular Matrices

Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening

Standardization and Confluence for a Lambda Calculus with Generalized Applications

Monotone Inductive and Coinductive Constructors of Rank 2

Generalized Iteration and Coiteration for Higher-Order Nested Datatypes

Recursion on Nested Datatypes in Dependent Type Theory

(Co-)Iteration for Higher-Order Nested Datatypes

Fixed Points of Type Constructors and Primitive Recursion

Interpolation for Natural Deduction with Generalized Eliminations

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

Monadic Translation of Intuitionistic Sequent Calculus

Parigot’s Second Order λμ-Calculus and Inductive Types

Monotone Fixed-Point Types and Strong Normalization

A Datastructure for Iterated Powers

Map fusion for nested datatypes in intensional type theory

Non-strictly positive fixed points for classical natural deduction

Iteration and coiteration schemes for higher-order and nested datatypes

Opcje filtrowania

Data publikacji

Dostępność treści

Typ publikacji

Słowa kluczowe

Zbiór danych

Czasopismo

INFONA - portal komunikacji naukowej

Wyniki wyszukiwania dla: Ralph Matthes

Dodaj adresata

Anulowanie wysłania wiadomości

Czy na pewno chcesz anulować wysłanie wiadomości?

Wyślij wiadomość

Opcje filtrowania

Data publikacji

Ustawianie zakresu dat

Podaj zakres dat dla filtrowania wyświetlonych wyników. Możesz podać datę początkową, końcową lub obie daty. Daty możesz wpisać ręcznie lub wybrać za pomocą kalendarza.

Dostępność treści

Typ publikacji

Słowa kluczowe

Zbiór danych

Czasopismo

Zgłaszanie błędu / nadużycia

Nieudane wysłanie zgłoszenia

Ułatwienia dostępu