Related papers: Inductive types in the Calculus of Algebraic Const…
We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational…
Concurrent pattern calculus (CPC) drives interaction between processes by comparing data structures, just as sequential pattern calculus drives computation. By generalising from pattern matching to pattern unification, interaction becomes…
A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer…
We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model constructions underlying forcing and realizability (both in intuitionistic and classical logic). The salient feature of this…
Many combinatorial proofs rely on induction. When these proofs are formulated in traditional language, they can be bulky and unmanageable. Coalgebras provide a language which can reduce reduce many inductive proofs in graded poset theory to…
In this paper, we introduce a general family of sequent-style calculi over the modal language and its fragments to capture the essence of all constructively acceptable systems. Calling these calculi \emph{constructive}, we show that any…
We present the Sequent Calculus Trainer, a tool that supports students in learning how to correctly construct proofs in the sequent calculus for first-order logic with equality. It is a proof assistant fostering the understanding of all the…
In the last few years appeared pedagogical propositional natural deduction systems. In these systems, one must satisfy the pedagogical constraint: the user must give an example of any introduced notion. First we expose the reasons of such a…
We show that when certain statements are provable in subsystems of constructive analysis using intuitionistic predicate calculus, related sequential statements are provable in weak classical subsystems. In particular, if a $\Pi^1_2$…
We define an extension of lambda-calculus with dependents types that enables us to encode transparent and opaque probabilistic programs and prove a strong normalisation result for it by a reducibility technique. While transparent…
This paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitary case of QW-types can be encoded using the combination of…
Transition Algebra (TA) is a type of infinite logic introduced to discuss rewriting systems. The natural deductive proof systems already introduced in TA satisfy completeness for countable signatures. However, it lacks compactness, making…
To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof assistants enforce this through syntactic conditions, which can…
Programs with control are usually modeled using lambda calculus extended with control operators. Instead of modifying lambda calculus, we consider a different model of computation. We introduce continuation calculus, or CC, a deterministic…
As dynamic and control systems become more complex, relying purely on numerical computations for systems analysis and design might become extremely expensive or totally infeasible. Computer algebra can act as an enabler for analysis and…
The Calculus of Audited Units (CAU) is a typed lambda calculus resulting from a computational interpretation of Artemov's Justification Logic under the Curry-Howard isomorphism; it extends the simply typed lambda calculus by providing…
This paper extends the dual calculus with inductive types and coinductive types. The paper first introduces a non-deterministic dual calculus with inductive and coinductive types. Besides the same duality of the original dual calculus, it…
We show that the first-order theory of structural subtyping of non-recursive types is decidable. Let $\Sigma$ be a language consisting of function symbols (representing type constructors) and $C$ a decidable structure in the relational…
Arithmetic circuits (AC) are circuits over the real numbers with 0/1-valued input variables whose gates compute the sum or the product of their inputs. Positive AC -- that is, AC representing non-negative functions -- subsume many…
We prove recursive formulas involving sums of divisors and sums of triangular numbers and give a variety of identities relating arithmetic functions to divisor functions providing inductive identities for such arithmetic functions.