Zobrazeno 1 - 10
of 36
pro vyhledávání: '"Basold, Henning"'
Directed topology is an area of mathematics with applications in concurrency. It extends the concept of a topological space by adding a notion of directedness, which restricts how paths can evolve through a space and enables thereby a faithful repres
Externí odkaz:
http://arxiv.org/abs/2312.06506
In this paper, we extend diagrammatic reasoning in monoidal categories with algebraic operations and equations. We achieve this by considering monoidal categories that are enriched in the category of Eilenberg-Moore algebras for a monad. Under the co
Externí odkaz:
http://arxiv.org/abs/2310.11288
Higher-dimensional automata (HDA) are a formalism to model the behaviour of concurrent systems. They are similar to ordinary automata but allow transitions in higher dimensions, effectively enabling multiple actions to happen simultaneously. For ordi
Externí odkaz:
http://arxiv.org/abs/2305.06428
Compositional methods are central to the development and verification of software systems. They allow to break down large systems into smaller components, while enabling reasoning about the behaviour of the composed system. For concurrent and communi
Externí odkaz:
http://arxiv.org/abs/2011.05712
Publikováno v:
Theory and Practice of Logic Programming, 2020
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 coind
Externí odkaz:
http://arxiv.org/abs/2008.03714
Publikováno v:
LNCS 11423 (2019) 783-813
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
Externí odkaz:
http://arxiv.org/abs/1811.07644
Autor:
Basold, Henning
The purpose of this paper is to develop and study recursive proofs of coinductive predicates. Such recursive proofs allow one to discover proof goals in the construction of a proof of a coinductive predicate, while still allowing the use of up-to tec
Externí odkaz:
http://arxiv.org/abs/1802.07143
Autor:
Basold, Henning, Geuvers, Herman
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
Externí odkaz:
http://arxiv.org/abs/1605.02206
Autor:
Basold, Henning
Publikováno v:
EPTCS 191, 2015, pp. 3-17
In this paper, I establish the categorical structure necessary to interpret dependent inductive and coinductive types. It is well-known that dependent type theories \`a la Martin-L\"of can be interpreted using fibrations. Modern theorem provers, howe
Externí odkaz:
http://arxiv.org/abs/1508.06779
Autor:
Basold, Henning
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 ac
Externí odkaz:
http://arxiv.org/abs/1403.2752