Lutz Schröder

IJCAI Conference 2025 Conference Paper

Non-expansive Fuzzy ALC

• Stefan Gebhart
• Lutz Schröder
• Paul Wild

Fuzzy description logics serve the representation of vague knowledge, typically letting concepts take truth degrees in the unit interval. Expressiveness, logical properties, and complexity vary strongly with the choice of propositional base. The Łukasiewicz propositional base is generally perceived to have preferable logical properties but often entails high complexity or even undecidability. Contrastingly, the less expressive Zadeh propositional base comes with low complexity but entails essentially no change in logical behaviour compared to the classical case. To strike a balance between these poles, we propose non-expansive fuzzy ALC, in which the Zadeh base is extended with Łukasiewicz connectives where one side is restricted to be a rational constant, that is, with constant shift operators. This allows, for instance, modelling dampened inheritance of properties along roles. We present an unlabelled tableau method for non-expansive fuzzy ALC, which allows reasoning over general TBoxes in EXPTime like in two-valued ALC.

CSL Conference 2025 Conference Paper

Quantitative Graded Semantics and Spectra of Behavioural Metrics

• Jonas Forster
• Lutz Schröder
• Paul Wild
• Harsh Beohar
• Sebastian Gurke
• Barbara König 0001
• Karla Messing

Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/ branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; in fact, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads, working in coalgebraic generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we introduce algebraic presentations of graded monads on the category of metric spaces. Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance. As a case study, we apply this criterion to obtain a new characteristic modal logic for trace distance in fuzzy metric transition systems.

AAAI Conference 2023 Conference Paper

Common Knowledge of Abstract Groups

• Merlin Humml
• Lutz Schröder

Epistemic logics typically talk about knowledge of individual agents or groups of explicitly listed agents. Often, however, one wishes to express knowledge of groups of agents specified by a given property, as in ‘it is common knowledge among economists’. We introduce such a logic of common knowledge, which we term abstract-group epistemic logic (AGEL). That is, AGEL features a common knowledge operator for groups of agents given by concepts in a separate agent logic that we keep generic, with one possible agent logic being ALC. We show that AGEL is EXPTIME-complete, with the lower bound established by reduction from standard group epistemic logic, and the upper bound by a satisfiability-preserving embedding into the full µ-calculus. Further main results include a finite model property (not enjoyed by the full µ-calculus) and a complete axiomatization.

CSL Conference 2023 Conference Paper

Quantitative Hennessy-Milner Theorems via Notions of Density

• Jonas Forster
• Sergey Goncharov 0001
• Dirk Hofmann
• Pedro Nora
• Lutz Schröder
• Paul Wild

The classical Hennessy-Milner theorem is an important tool in the analysis of concurrent processes; it guarantees that any two non-bisimilar states in finitely branching labelled transition systems can be distinguished by a modal formula. Numerous variants of this theorem have since been established for a wide range of logics and system types, including quantitative versions where lower bounds on behavioural distance (e. g. in weighted, metric, or probabilistic transition systems) are witnessed by quantitative modal formulas. Both the qualitative and the quantitative versions have been accommodated within the framework of coalgebraic logic, with distances taking values in quantales, subject to certain restrictions, such as being so-called value quantales. While previous quantitative coalgebraic Hennessy-Milner theorems apply only to liftings of set functors to (pseudo)metric spaces, in the present work we provide a quantitative coalgebraic Hennessy-Milner theorem that applies more widely to functors native to metric spaces; notably, we thus cover, for the first time, the well-known Hennessy-Milner theorem for continuous probabilistic transition systems, where transitions are given by Borel measures on metric spaces, as an instance of such a general result. In the process, we also relax the restrictions imposed on the quantale, and additionally parametrize the technical account over notions of closure and, hence, density, providing associated variants of the Stone-Weierstraß theorem; this allows us to cover, for instance, behavioural ultrametrics.

FSCD Conference 2022 Conference Paper

Stateful Structural Operational Semantics

• Sergey Goncharov 0001
• Stefan Milius
• Lutz Schröder
• Stelios Tsampas 0001
• Henning Urbat

Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences.

MFCS Conference 2021 Conference Paper

A Linear-Time Nominal μ-Calculus with Name Allocation

• Daniel Hausmann 0001
• Stefan Milius
• Lutz Schröder

Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding nominal automata models such as {regular nondeterministic nominal automata (RNNAs)} have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Bar-μTL} for finite words over an infinite alphabet, which features full negation and freeze quantification via name binding. We show by a nontrivial reduction to extended regular nondeterministic nominal automata that even though Bar-μTL} allows unrestricted nondeterminism and unboundedly many registers, model checking Bar-μTL} over RNNAs and satisfiability checking both have elementary complexity. For example, model checking is in 2ExpSpace, more precisely in parametrized ExpSpace, effectively with the number of registers as the parameter.

TCS Journal 2021 Journal Article

A metalanguage for guarded iteration

• Sergey Goncharov
• Christoph Rauch
• Lutz Schröder

Notions of guardedness serve to delineate admissible recursive definitions in various settings in a compositional manner. In recent work, we have introduced an axiomatic notion of guardedness in symmetric monoidal categories, which serves as a unifying framework for various examples from program semantics, process algebra, and beyond. In the present paper, we propose a generic metalanguage for guarded iteration based on combining this notion with the fine-grain call-by-value paradigm, which we intend as a unifying programming language for guarded and unguarded iteration in the presence of computational effects. We give a generic (categorical) semantics of this language over a suitable class of strong monads supporting guarded iteration, and show it to be in touch with the standard operational behaviour of iteration by giving a concrete big-step operational semantics for a certain specific instance of the metalanguage and establishing soundness and (computational) adequacy for this case.

CSL Conference 2021 Conference Paper

The Alternating-Time μ-Calculus with Disjunctive Explicit Strategies

• Merlin Göttlinger
• Lutz Schröder
• Dirk Pattinson

Alternating-time temporal logic (ATL) and its extensions, including the alternating-time µ-calculus (AMC), serve the specification of the strategic abilities of coalitions of agents in concurrent game structures. The key ingredient of the logic are path quantifiers specifying that some coalition of agents has a joint strategy to enforce a given goal. This basic setup has been extended to let some of the agents (revocably) commit to using certain named strategies, as in ATL with explicit strategies (ATLES). In the present work, we extend ATLES with fixpoint operators and strategy disjunction, arriving at the alternating-time µ-calculus with disjunctive explicit strategies (AMCDES), which allows for a more flexible formulation of temporal properties (e. g. fairness) and, through strategy disjunction, a form of controlled non-determinism in commitments. Our main result is an ExpTime upper bound for satisfiability checking (which is thus ExpTime-complete). We also prove upper bounds QP (quasipolynomial time) and NP∩coNP for model checking under fixed interpretations of explicit strategies, and NP under open interpretation. Our key technical tool is a treatment of the AMCDES within the generic framework of coalgebraic logic, which in particular reduces the analysis of most reasoning tasks to the treatment of a very simple one-step logic featuring only propositional operators and next-step operators without nesting; we give a new model construction principle for this one-step logic that relies on a set-valued variant of first-order resolution.

IJCAI Conference 2019 Conference Paper

A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic

• Paul Wild
• Lutz Schröder
• Dirk Pattinson
• Barbara König

The fuzzy modality probably is interpreted over probabilistic type spaces by taking expected truth values. The arising probabilistic fuzzy description logic is invariant under probabilistic bisimilarity; more informatively, it is non-expansive wrt. a suitable notion of behavioural distance. In the present paper, we provide a characterization of the expressive power of this logic based on this observation: We prove a probabilistic analogue of the classical van Benthem theorem, which states that modal logic is precisely the bisimulation-invariant fragment of first-order logic. Specifically, we show that every formula in probabilistic fuzzy first-order logic that is non-expansive wrt. behavioural distance can be approximated by concepts of bounded rank in probabilistic fuzzy description logic.

IJCAI Conference 2017 Conference Paper

A Characterization Theorem for a Modal Description Logic

• Paul Wild
• Lutz Schröder

Modal description logics feature modalities that capture dependence of knowledge on parameters such as time, place, or the information state of agents. E. g. , the logic S5-ALC combines the standard description logic ALC with an S5-modality that can be understood as an epistemic operator or as representing (undirected) change. This logic embeds into a corresponding modal first-order logic S5-FOL. We prove a modal characterization theorem for this embedding, in analogy to results by van Benthem and Rosen relating ALC to standard first-order logic: We show that S5-ALC with only local roles is, both over finite and over unrestricted models, precisely the bisimulation-invariant fragment of S5-FOL, thus giving an exact description of the expressive power of S5-ALC with only local roles.

JAIR Journal 2017 Journal Article

Probabilistic Description Logics for Subjective Uncertainty

• Victor Gutierrez-Basulto
• Jean Christoph Jung
• Carsten Lutz
• Lutz Schröder

We propose a family of probabilistic description logics (DLs) that are derived in a principled way from Halpern's probabilistic first-order logic. The resulting probabilistic DLs have a two-dimensional semantics similar to temporal DLs and are well-suited for representing subjective probabilities. We carry out a detailed study of reasoning in the new family of logics, concentrating on probabilistic extensions of the DLs ALC and EL, and showing that the complexity ranges from PTime via ExpTime and 2ExpTime to undecidable.

TIME Conference 2015 Conference Paper

Global Caching for the Flat Coalgebraic µ-Calculus

• Daniel Hausmann 0001
• Lutz Schröder

Branching-time temporal logics generalizing relational temporal logics such as CTL have been proposed for various system types beyond the purely relational world. This includes, e. g. , alternating-time logics, which talk about winning strategies over concurrent game structures, and Parikh's game logic, which is interpreted over monotone neighbourhood frames, as well as probabilistic fixpoint logics. Coalgebraic logic has emerged as a unifying semantic and algorithmic framework for logics featuring generalized modalities of this type. Here, we present a generic global caching algorithm for satisfiability checking in the flat coalgebraic mu-calculus, which realizes known tight exponential-time upper complexity bounds but offers potential for heuristic optimization. It is based on a tableau system that makes do without additional labelling of nodes beyond formulas from the standard Fischer-Ladner closure, such as foci or termination counters for eventualities. Moreover, the tableau system is single-pass, i. e. avoids building an exponential-sized structure in a first pass, to our best knowledge, optimal single-pass systems without numeric time-outs were not previously available even for CTL.

I&C Journal 2013 Journal Article

A coinductive calculus for asynchronous side-effecting processes

• Sergey Goncharov
• Lutz Schröder

We present an abstract framework for concurrent processes in which atomic steps have generic side effects, handled according to the principle of monadic encapsulation of effects. Processes in this framework are potentially infinite resumptions, modelled using final coalgebras over the monadic base. As a calculus for such processes, we introduce a concurrent extension of Moggiʼs monadic meta-language of effects. We establish soundness and completeness of a natural equational axiomatization of this calculus. Our main result is a corecursion scheme that is explicitly definable over the base language and provides flexible expressive means for the definition of new operators on processes, such as parallel composition. Moreover, we present initial results on verification methods for generic side-effecting processes.

IJCAI Conference 2013 Conference Paper

Syntactic Labelled Tableaux for Łukasiewicz Fuzzy ALC

• Agnieszka Kułacka
• Dirk Pattinson
• Lutz Schröder

Fuzzy description logics (DLs) serve as a tool to handle vagueness in real-world knowledge. There is particular interest in logics implementing Łukasiewicz semantics, which has a number of favourable properties. Current decision procedures for Łukasiewicz fuzzy DLs work by reduction to exponentially large mixed integer programming problems. Here, we present a decision method that stays closer to logical syntax, a labelled tableau algorithm for Łukasiewicz Fuzzy ALC that calls only on (pure) linear programming, and this only to decide atomic clashes. The algorithm realizes the best known complexity bound, NEXP- TIME. Our language features a novel style of fuzzy ABoxes that work with comparisons of truth degrees rather than explicit numerical bounds.

AAAI Conference 2011 Conference Paper

A Closer Look at the Probabilistic Description Logic Prob-EL

• Víctor Gutiérrez Basulto
• Jean Christoph Jung
• Carsten Lutz
• Lutz Schröder

We study probabilistic variants of the description logic EL. For the case where probabilities apply only to concepts, we provide a careful analysis of the borderline between tractability and EXPTIME-completeness. One outcome is that any probability value except zero and one leads to intractability in the presence of general TBoxes, while this is not the case for classical TBoxes. For the case where probabilities can also be applied to roles, we show PSPACE-completeness. This result is (positively) surprising as the best previously known upper bound was 2-EXPTIME and there were reasons to believe in completeness for this class.

I&C Journal 2010 Journal Article

Cut elimination in coalgebraic logics

• Dirk Pattinson
• Lutz Schröder

We give two generic proofs for cut elimination in propositional modal logics, interpreted over coalgebras. We first investigate semantic coherence conditions between the axiomatisation of a particular logic and its coalgebraic semantics that guarantee that the cut-rule is admissible in the ensuing sequent calculus. We then independently isolate a purely syntactic property of the set of modal rules that guarantees cut elimination. Apart from the fact that cut elimination holds, our main result is that the syntactic and semantic assumptions are equivalent in case the logic is amenable to coalgebraic semantics. As applications we present a new proof of the (already known) interpolation property for coalition logic and newly establish the interpolation property for the conditional logics LCK and LCKID.

ECAI Conference 2010 Conference Paper

Optimal Tableaux for Conditional Logics with Cautious Monotonicity

• Lutz Schröder
• Dirk Pattinson
• Daniel Hausmann 0001

Conditional logics capture default entailment in a modal framework in which non-monotonic implication is a first-class citizen, and in particular can be negated and nested. There is a wide range of axiomatizations of conditionals in the literature, from weak systems such as the basic conditional logic CK, which allows only for equivalent exchange of conditional antecedents, to strong systems such as Burgess' system 𝒮 , which imposes the full Kraus-Lehmann-Magidor properties of preferential logic. While tableaux systems implementing the actual complexity of the logic at hand have recently been developed for several weak systems, strong systems including in particular disjunction elimination or cautious monotonicity have so far eluded such efforts; previous results for strong systems are limited to semantics-based decision procedures and completeness proofs for Hilbert-style axiomatizations. Here, we present tableaux systems of optimal complexity PSPACE for several strong axiom systems in conditional logic, including system 𝒮 ; the arising decision procedure for system 𝒮 is implemented in the generic reasoning tool CoLoSS.

KR Conference 2010 Conference Paper

Probabilistic Description Logics for Subjective Uncertainty

• Carsten Lutz
• Lutz Schröder

regarding the general way in which probabilities are used, We propose a new family of probabilistic description logics (DLs) that, in contrast to most existing approaches, are derived in a principled way from Halpern’s probabilistic firstorder logic. The resulting probabilistic DLs have a twodimensional semantics similar to certain popular combinations of DLs with temporal logic and are well-suited for capturing subjective probabilities. Our main contribution is a detailed study of the complexity of reasoning in the new family of probabilistic DLs, showing that it ranges from PT IME for weak variants based on the lightweight DL EL to undecidable for some expressive variants based on the DL ALC. Motivation

IJCAI Conference 2009 Conference Paper

• Lutz Schröder
• Dirk Pattinson
• Clemens Kupke

It has been recognised that the expressivity of description logics benefits from the introduction of non-standard modal operators beyond existential and number restrictions. Such operators support notions such as uncertainty, defaults, agency, obligation, or evidence, whose semantics often lies outside the realm of relational structures. Coalgebraic hybrid logic serves as a unified setting for logics that combine non-standard modal operators and nominals, which allow reasoning about individuals. In this framework, we prove a generic EXPTIME upper bound for concept satisfiability over general TBoxes, which instantiates to novel upper bounds for many individual logics including probabilistic logic with nominals.

TCS Journal 2009 Journal Article

HasCasl: Integrated higher-order specification and program development

• Lutz Schröder
• Till Mossakowski

We lay out the design of HasCasl, a higher order extension of the algebraic specification language Casl that serves both as a wide-spectrum language for the rigorous specification and development of software, in particular but not exclusively in modern functional programming languages, and as an expressive standard language for higher-order logic. Distinctive features of HasCasl include partial higher order functions, higher order subtyping, shallow polymorphism, and an extensive type-class mechanism. Moreover, HasCasl provides dedicated specification support for monad-based functional-imperative programming with generic side effects, including a monad-based generic Hoare logic.

TCS Journal 2008 Journal Article

Expressivity of coalgebraic modal logic: The limits and beyond

• Lutz Schröder

Modal logic has a good claim to being the logic of choice for describing the reactive behaviour of systems modelled as coalgebras. Logics with modal operators obtained from so-called predicate liftings have been shown to be invariant under behavioural equivalence. Expressivity results stating that, conversely, logically indistinguishable states are behaviourally equivalent depend on the existence of separating sets of predicate liftings for the signature functor at hand. Here, we provide a classification result for predicate liftings which leads to an easy criterion for the existence of such separating sets, and we give simple examples of functors that fail to admit expressive normal or monotone modal logics, respectively, or in fact an expressive (unary) modal logic at all. We then move on to polyadic modal logic, where modal operators may take more than one argument formula. We show that every accessible functor admits an expressive polyadic modal logic. Moreover, expressive polyadic modal logics are, unlike unary modal logics, compositional.

KR Conference 2008 Conference Paper

How Many Toes Do I Have? Parthood and Number Restrictions in Description Logics

• Lutz Schröder
• Dirk Pattinson

The modelling of parthood relations in description logics via transitive roles often leads to undecidability when combined with number restrictions and role hierarchies. Here, we introduce the description logic PHQ that explicitly supports reasoning about parthood in the presence of qualified number restrictions. Our main results are completeness and decidability in NEXPTIME. Conceptually, we argue that PHQ provides a better semantic fit for many applications: more often than not, parthoods occurring e. g. in biomedical ontologies are expected to be tree-like. In such cases, PHQ supports stronger inferences than standard description logics. Technically this is achieved by explicitly excluding the merging of descendants, which, at the same time, eliminates the prime source of undecidability. We work in the general setting of coalgebraic modal logic, a generic semantic framework for not-necessarily-normal modal logics. This added generality allows the re-use of many of our results for other logics of sometimes quite different flavour.

TCS Journal 2006 Journal Article

A coalgebraic approach to the semantics of the ambient calculus

• Daniel Hausmann
• Till Mossakowski
• Lutz Schröder

Recently, various process calculi have been introduced which are suited for the modelling of mobile computation and in particular the mobility of program code; a prominent example is the ambient calculus. Due to the complexity of the involved spatial reduction, there is—in contrast to the situation in standard process algebra—up to now no satisfying coalgebraic representation of a mobile process calculus. Here, we discuss a coalgebraic denotational semantics for the ambient calculus, viewed as a step towards a generic coalgebraic framework for modelling mobile systems. Crucial features of our modelling are a set of GSOS style transition rules for the ambient calculus, a hardwiring of the so-called hardening relation in the functorial signature, and a set-based treatment of hidden name sharing. The formal representation of this framework is cast in the algebraic–coalgebraic specification language COCASL.

IROS Conference 2006 Conference Paper

Closing a Million-Landmarks Loop

• Udo Frese
• Lutz Schröder

We present an improved version of the treemap SLAM algorithm which uses Cholesky factors for representing Gaussians and a hierarchical tree partitioning algorithm derived from the established Kernighan-Lin heuristic for graph bisection. We demonstrate the algorithm's efficiency by mapping a simulated building with 1032271 landmarks. In the end, we close a million-landmarks loop in 21 ms, providing an estimate for ap10000 selected landmarks close to the robot, or in 442 ms for computing a full estimate

MFCS Conference 2006 Conference Paper

Completeness of Global Evaluation Logic

• Sergey Goncharov 0001
• Lutz Schröder
• Till Mossakowski

Abstract Monads serve the abstract encapsulation of side effects in semantics and functional programming. Various monad-based specification languages have been introduced in order to express requirements on generic side-effecting programs. A basic role is played here by global evaluation logic, concerned with formulae which may be thought of as being universally quantified over the state space; this formalism is the fundament of more advanced logics such as monad-based Hoare logic or dynamic logic. We prove completeness of global evaluation logic for models in cartesian categories with a distinguished Heyting algebra object.

TCS Journal 2006 Journal Article

The HASCASL prologue: Categorical syntax and semantics of the partial λ -calculus

• Lutz Schröder

We develop the semantic foundations of the specification language HASCASL, which combines algebraic specification and functional programming on the basis of Moggi's partial λ -calculus. Generalizing Lambek's classical equivalence between the simply typed λ -calculus and cartesian closed categories, we establish an equivalence between partial cartesian closed categories (pccc's) and partial λ -theories. Building on these results, we define (set-theoretic) notions of intensional Henkin model and syntactic λ -algebra for Moggi's partial λ -calculus. These models are shown to be equivalent to the originally described categorical models in pccc's via the global element construction. The semantics of HASCASL is defined in terms of syntactic λ -algebras. Correlations between logics and classes of categories facilitate reasoning both on the logical and on the categorical side; as an application, we pinpoint unique choice as the distinctive feature of topos logic (in comparison to intuitionistic higher-order logic of partial functions, which by our results is the logic of pccc's with equality). Finally, we give some applications of the model-theoretic equivalence result to the semantics of HASCASL and its relation to first-order CASL.

TCS Journal 2005 Journal Article

Amalgamation in the semantics of CASL

• Lutz Schröder
• Till Mossakowski
• Andrzej Tarlecki
• Bartek Klin
• Piotr Hoffman

We present a semantics for architectural specifications in the Common Algebraic Specification Language (Casl), including an extended static analysis compatible with model-theoretic requirements. The main obstacle here is the lack of amalgamation for Casl models. To circumvent this problem, we extend the Casl logic by introducing enriched signatures, where subsort embeddings form a category rather than just a preorder. The extended model functor satisfies the amalgamation property as well as its converse, which makes it possible to express the amalgamability conditions in the semantic rules in static terms. Using these concepts, we develop the semantics at various levels in an institution-independent fashion. Moreover, amalgamation for enriched Casl means that a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for Casl.

CSL Conference 2004 Conference Paper

The Logic of the Partial lambda-Calculus with Equality

• Lutz Schröder

Abstract We investigate the logical aspects of the partial λ -calculus with equality, exploiting an equivalence between partial λ -theories and partial cartesian closed categories (pcccs) established here. The partial λ -calculus with equality provides a full-blown intuitionistic higher order logic, which in a precise sense turns out to be almost the logic of toposes, the distinctive feature of the latter being unique choice. We give a linguistic proof of the generalization of the fundamental theorem of toposes to pcccs with equality; type theoretically, one thus obtains that the partial λ -calculus with equality encompasses a Martin-Löf-style dependent type theory. This work forms part of the semantical foundations for the higher order algebraic specification language HasCasl.

CSL Conference 2003 Conference Paper

Henkin Models of the Partial sigma-Calculus

• Lutz Schröder

Abstract We define (set-theoretic) notions of intensional Henkin model and syntactic λ -algebra for Moggi’s partial λ -calculus. These models are shown to be equivalent to the originally described categorical models via the global element construction; the proof makes use of a previously introduced construction of classifying categories. The set-theoretic semantics thus obtained is the foundation of the higher order algebraic specification language HasCasl, which combines specification and functional programming.

MFCS Conference 2001 Conference Paper

Checking Amalgamability Conditions for C ASL Architectural Specifications

• Bartek Klin
• Piotr Hoffman
• Andrzej Tarlecki
• Lutz Schröder
• Till Mossakowski

Abstract scC ASL, a specification formalism developed recently by the CoFI group, offers architectural specifications as a way to describe how simpler modules can be used to construct more complex ones. The semantics for C asl architectural specifications formulates static amalgamation conditions as a prerequisite for such constructions to be well-formed. These are non-trivial in the presence of subsorts due to the failure of the amalgamation property for the C ASL institution. We show that indeed the static amalgamation conditions for C ASL are undecidable in general. However, we identify a number of practically relevant special cases where the problem becomes decidable and analyze its complexity there. In cases where the result turns out to be PSPACE -hard, we discuss further restrictions under which polynomial algorithms become available. All this underlies the static analysis as implemented in the C ASL tool set.

CSL Conference 2001 Conference Paper

Life without the Terminal Type

• Lutz Schröder

Abstract We introduce a method of extending arbitrary categories by a terminal object and apply this method in various type theoretic settings. In particular, we show that categories that are cartesian closed except for the lack of a terminal object have a universal full extension to a cartesian closed category, and we characterize categories for which the latter category is a topos. Both the basic construction and its correctness proof are extremely simple. This is quite surprising in view of the fact that the corresponding results for the simply typed λ-calculus with surjective pairing, in particular concerning the decision problem for equality of terms in the presence of a terminal type, are comparatively involved.