Type systems certify program properties in a compositional way. From a bigger program one can abstract out a part and certify the properties of the resulting abstract program by just using the type ...of the part that was abstracted away. Termination and productivity are non-trivial yet desired program properties, and several type systems have been put forward that guarantee termination, compositionally. These type systems are intimately connected to the definition of least and greatest fixed-points by ordinal iteration. While most type systems use conventional iteration, we consider inflationary iteration in this article. We demonstrate how this leads to a more principled type system, with recursion based on well-founded induction. The type system has a prototypical implementation, MiniAgda, and we show in particular how it certifies productivity of corecursive and mixed recursive-corecursive functions.
Normalization fails in type theory with an impredicative universe of propositions and a proof-irrelevant propositional equality. The counterexample to normalization is adapted from Girard's ...counterexample against normalization of System F equipped with a decider for type equality. It refutes Werner's normalization conjecture published in LMCS Wer08.
Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent ...and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism. To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language, MiniAgda, with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by concepts such as inaccessible patterns and parametric function spaces. This paper provides an introduction to MiniAgda by example and informal explanations of the underlying principles.
Dependently typed programs contain an excessive amount of static terms which
are necessary to please the type checker but irrelevant for computation. To
separate static and dynamic code, several ...static analyses and type systems have
been put forward. We consider Pfenning's type theory with irrelevant
quantification which is compatible with a type-based notion of equality that
respects eta-laws. We extend Pfenning's theory to universes and large
eliminations and develop its meta-theory. Subject reduction, normalization and
consistency are obtained by a Kripke model over the typed equality judgement.
Finally, a type-directed equality algorithm is described whose completeness is
proven by a second Kripke model.
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 ...in the type system that
recursive calls occur just at a smaller size. This approach is only sound if
the type of the recursive function is admissible, i.e., depends on the size
index in a certain way. To explore the space of admissible functions in the
presence of higher-kinded data types and impredicative polymorphism, a
semantics is developed where sized types are interpreted as functions from
ordinals into sets of strongly normalizing terms. It is shown that upper
semi-continuity of such functions is a sufficient semantic criterion for
admissibility. To provide a syntactical criterion, a calculus for
semi-continuous functions is developed.
In this paper, we present an Agda formalization of a normalizer for simply-typed lambda terms. The normalizer consists of two coinductively defined functions in the delay monad: One is a standard ...evaluator of lambda terms to closures, the other a type-directed reifier from values to h-long b-normal forms. Their composition, normalization-by-evaluation, is shown to be a total function a posteriori, using a standard logical-relations argument. The successful formalization serves as a proof-of-concept for coinductive programming and reasoning using sized types and copatterns, a new and presently experimental feature of Agda.
Abstract
In a dependently typed language, we can guarantee correctness of our programmes by providing formal proofs. To check them, the typechecker elaborates these programs and proofs into a ...low-level core language. However, this core language is by nature hard to understand by mere humans, so how can we know we proved the right thing? This question occurs in particular for dependent copattern matching, a powerful language construct for writing programmes and proofs by dependent case analysis and mixed induction/coinduction. A definition by copattern matching consists of a list of
clauses
that are elaborated to a
case tree
, which can be further translated to primitive
eliminators
. In previous work this second step has received a lot of attention, but the first step has been mostly ignored so far. We present an algorithm elaborating definitions by dependent copattern matching to a core language with inductive data types, coinductive record types, an identity type, and constants defined by well-typed case trees. To ensure correctness, we prove that elaboration preserves the first-match semantics of the user clauses. Based on this theoretical work, we reimplement the algorithm used by Agda to check left-hand sides of definitions by pattern matching. The new implementation is at the same time more general and less complex, and fixes a number of bugs and usability issues with the old version. Thus, we take another step towards the formally verified implementation of a practical dependently typed language.
Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful ...extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.
An automated optical biosensor system based on fluorescence excitation and detection in the evanescent field of a quartz fiber was used to detect 16-mer oligonucleotides in DNA hybridization assays. ...A biotinylated capture probe was immobilized on the fiber surface via avidin or streptavidin. The hybridization with fluorescein-labeled complementary strands was monitored in real time by fluorescence detection. The double strands formed by hybridization could be dissociated by chemical or thermal regeneration, allowing one to perform hundreds of assay cycles with the same fiber. The signal loss during long-time measurements, i.e., consecutive hybridization assays, can be described by a single-exponential function. Over more than 200 cycles, the net signal decreased by 50% with a signal variation of 2.4% after correction for this signal loss. By binding the capture probe with the 5‘-end to the optical fiber surface, and by using a 50% (w/w) aqueous urea solution for chemical regeneration, the duration of an assay cycle could be reduced to 3 min. By applying longer assay cycles, the detection limit for the hybridization with a complementary fluorescein-labeled oligonucleotide was 2.0 × 10-13 M (24 fmol). To detect an unlabeled complementary 16-mer oligonucleotide, competitive hybridization assays were performed, resulting in a detection limit of 1.1 × 10-9 M (132 pmol). Poly(acrylic acid) 5100 sodium salt and Tween 20 were used in the hybridization buffer to prevent nonspecific binding caused by ionic or hydrophobic interaction. The amount of nonspecific binding of noncomplementary oligonucleotides was in the range of 1−2%, compared with the specific binding in the different hybridization assays.
Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful ...extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types (HITs). This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of HITs. These new primitives allow the direct definition of function and propositional extensionality as well as quotient types, all with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. The adoption of cubical type theory extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.
PDF
