A cartesian-closed category for higher-order model checking

2017 ◽  
Author(s):  
Martin Hofmann ◽  
Jeremy Ledent
Keyword(s):  
Model Checking ◽  
Higher Order ◽  
Order Model ◽  
Cartesian Closed Category ◽  
Closed Category ◽  
Cartesian Closed

Automata theory and higher-order model-checking

2016 ◽  
Vol 3 (4) ◽  
pp. 13-31 ◽  
Author(s):  
Igor Walukiewicz
Keyword(s):  
Model Checking ◽  
Higher Order ◽  
Automata Theory ◽  
Order Model

Predicate abstraction and CEGAR for higher-order model checking

2011 ◽  
Vol 46 (6) ◽  
pp. 222-233 ◽  
Author(s):  
Naoki Kobayashi ◽  
Ryosuke Sato ◽  
Hiroshi Unno
Keyword(s):  
Model Checking ◽  
Higher Order ◽  
Predicate Abstraction ◽  
Order Model

An enrichment theorem for an axiomatisation of categories of domains and continuous functions

1997 ◽  
Vol 7 (5) ◽  
pp. 591-618 ◽  
Author(s):  
MARCELO P. FIORE
Keyword(s):  
Fixed Point ◽  
Continuous Functions ◽  
Domain Theory ◽  
Cartesian Closed Category ◽  
Closed Category ◽  
Cartesian Closed

Domain-theoretic categories are axiomatised by means of categorical non-order-theoretic requirements on a cartesian closed category equipped with a commutative monad. In this paper we prove an enrichment theorem showing that every axiomatic domain-theoretic category can be endowed with an intensional notion of approximation, the path relation, with respect to which the category Cpo-enriches.Our analysis suggests more liberal notions of domains. In particular, we present a category where the path order is not ω-complete, but in which the constructions of domain theory (such as, for example, the existence of uniform fixed-point operators and the solution of domain equations) are available.

Monad compositions II: Kleisli strength

2008 ◽  
Vol 18 (3) ◽  
pp. 613-643 ◽  
Author(s):  
ERNIE MANES ◽  
PHILIP MULRY
Keyword(s):  
Monoidal Category ◽  
Linear Equations ◽  
Large Collection ◽  
Data Types ◽  
Cartesian Closed Category ◽  
Closed Category ◽  
Symmetric Monoidal Category ◽  
Cartesian Closed

In this paper we introduce the concept of Kleisli strength for monads in an arbitrary symmetric monoidal category. This generalises the notion of commutative monad and gives us new examples, even in the cartesian-closed category of sets. We exploit the presence of Kleisli strength to derive methods for generating distributive laws. We also introduce linear equations to extend the results to certain quotient monads. Mechanisms are described for finding strengths that produce a large collection of new distributive laws, and consequently monad compositions, including the composition of monadic data types such as lists, trees, exceptions and state.

Sign in / Sign up

Export Citation Format

Share Document