Related papers: Global semantic typing for inductive and coinducti…
We present an elaboration of inductive definitions down to a universe of datatypes. The universe of datatypes is an internal presentation of strictly positive families within type theory. By elaborating an inductive definition -- a…
This is the fourth in a series of papers extending Martin-L\"of's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define cubical type systems supporting a general schema of…
Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this paper we show how inductive datatypes may be added to the quantum programming language QPL.…
In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inference rules. We propose an extension of the Curry-Howard…
We introduce an operational rewriting-based semantics for strictly positive nested higher-order (co)inductive types. The semantics takes into account the "limits" of infinite reduction sequences. This may be seen as a refinement and…
We propose a method to adapt functional logic programming to deal with reasoning on coinductively interpreted programs as well as on inductively interpreted programs. In order to do so, we consider a class of objects interesting for this…
Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-L\"of's meaning explanations for constructive type theory define the concept of a type in…
In the impredicative type theory of System F ({\lambda}2), it is possible to create inductive data types, such as natural numbers and lists. It is also possible to create coinductive data types such as streams. They work well in the sense…
We develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theory with a small set of rules, while still being fairly…
We need much better understanding of information processing and computation as its primary form. Future progress of new computational devices capable of dealing with problems of big data, internet of things, semantic web, cognitive robotics…
A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations,…
Type theories can be formalized using the intrinsically (hard) or the extrinsically (soft) typed style. In large libraries of type theoretical features, often both styles are present, which can lead to code duplication and integration…
Recently we presented a concise survey of the formulation of the induction and coinduction principles, and some concepts related to them, in programming languages type theory and four other mathematical disciplines. The presentation in type…
The Curry-Howard correspondence is about a relationship between types and programs on the one hand and propositions and proofs on the other. The implications for programming language design and program verification is an active field of…
Metatheorems about type theories are often proven by interpreting the syntax into models constructed using categorical gluing. We propose to use only sconing (gluing along a global section functor) instead of general gluing. The sconing is…
This is the second in a series of papers extending Martin-L\"{o}f's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for simple types developed in Part I,…
Many formal languages of contemporary mathematical music theory -- particularly those employing category theory -- are powerful but cumbersome: ideas that are conceptually simple frequently require expression through elaborate categorical…
In the pure Calculus of Constructions (CC) one can define data types and function over these, and there is a powerful higher order logic to reason over these functions and data types. This is due to the combination of impredicativity and…
This reports introduces a novel sound and complete semantics for first order intuitionistic logic, in the framework of category theory and by the computational interpretation of the logic based on the so-called Curry-Howard isomorphism.…
The logical parallelism of propositional connectives and type constructors extends beyond the static realm of predicates, to the dynamic realm of processes. Understanding the logical parallelism of process propositions and dynamic types was…