Source author record

Henning Basold

Henning Basold appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science Programming Languages

Catalog footprint

What is connected

5works

2topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2022arXiv

Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses

We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive uniform proofs; its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality; and soundness of both proof systems is proven relative to a novel coalgebraic description of complete Herbrand models.

preprint2020arXiv

The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them

In sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen's classical and intuitionistic calculi LK and LJ enjoy cut elimination. The property is less studied in coinductive extensions of sequent calculi. In this paper, we use coinductive Horn clause theories to show that cut is not eliminable in a coinductive extension of LJ, a system we call CLJ. We derive two further practical results from this study. We show that CoLP by Gupta et al. gives rise to cut-free proofs in CLJ with fixpoint terms, and we formulate and implement a novel method of coinductive theory exploration that provides several heuristics for discovery of cut formulae in CLJ.

preprint2016arXiv

Type Theory based on Dependent Inductive and Coinductive Types

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 expressive. For example, all well-known basic types and type formers that are needed for using this type theory as a logic are definable: propositional connectives, like falsity, conjunction, disjunction, and function space, dependent function space, existential quantification, equality, natural numbers, vectors etc. The reduction relation on terms consists solely of a rule for recursion and a rule for corecursion. The reduction relations for well-known types arise from that. To further support the introduction of this new type theory, we also prove fundamental properties of its term calculus. Most importantly, we prove subject reduction and strong normalisation of the reduction relation, which gives computational meaning to the terms. The presented type theory is based on ideas from categorical logic that have been investigated before by the first author, and it extends Hagino's categorical data types to a dependently typed setting. By basing the type theory on concepts from category theory we maintain the duality between inductive and coinductive types, and it allows us to describe, for example, the function space as a coinductive type.

preprint2015arXiv

Dependent Inductive and Coinductive Types are Fibrational Dialgebras

In this paper, I establish the categorical structure necessary to interpret dependent inductive and coinductive types. It is well-known that dependent type theories à la Martin-Löf can be interpreted using fibrations. Modern theorem provers, however, are based on more sophisticated type systems that allow the definition of powerful inductive dependent types (known as inductive families) and, somewhat limited, coinductive dependent types. I define a class of functors on fibrations and show how data type definitions correspond to initial and final dialgebras for these functors. This description is also a proposal of how coinductive types should be treated in type theories, as they appear here simply as dual of inductive types. Finally, I show how dependent data types correspond to algebras and coalgebras, and give the correspondence to dependent polynomial functors.

preprint2014arXiv

Transformation von Scade-Modellen zur SMT-basierten Verifikation

In this work we develop a fully automatic verification procedure of safety properties of Scade programs. We transform each such program into an SMT instance (Satisfiability Modulo Theories) and feed this to a solver. The goal is to have a publicly accessible experimentation platform for the verification of Scade programs. The choice of SMT is determined by the fact that it offers more expressive logics than propositional logic, yet their solvers have been shown to perform very well. The expressiveness of SMT logics allows us to implement symbolic model checking thus avoiding the expansion of the complete state space of the models during the verification. In order to reduce the complexity we transform the Scade programs into SMT instances in two steps. First they are reduced to programs of a synchronous data flow language Lama. This language has simpler semantics than Scade while still preserving some of the programmer's abstractions. Next we interpret such a Lama program as a system of quantifier free first-order formulas. The remaining abstractions in Lama can be used to simplify these systems. This in turn could lead to speeding up the verification process and allowing more properties to be verifiable. We implemented these transformations successfully in a software using Haskell. This work is concluded by a comparison of this software to the existing verification software "Scade Design Verifier" which comes with the Scade Suite.