Showing 1–13 of 13 results for author: Kavvos, G A

Two-dimensional Kripke Semantics II: Stability and Completeness

Authors: G. A. Kavvos

Abstract: We revisit the duality between Kripke and algebraic semantics of intuitionistic and intuitionistic modal logic. We find that there is a certain mismatch between the two semantics, which means that not all algebraic models can be embedded into a Kripke model. This leads to an alternative proposal for a relational semantics, the stable semantics. Instead of an arbitrary partial order, the stable sem… ▽ More We revisit the duality between Kripke and algebraic semantics of intuitionistic and intuitionistic modal logic. We find that there is a certain mismatch between the two semantics, which means that not all algebraic models can be embedded into a Kripke model. This leads to an alternative proposal for a relational semantics, the stable semantics. Instead of an arbitrary partial order, the stable semantics requires a distributive lattice of worlds. We constructively show that the stable semantics is exactly as complete as the algebraic semantics. Categorifying these results leads to a 2-duality between two-dimensional stable semantics and categories of product-preserving presheaves, i.e. models of algebraic theories in the style of Lawvere. △ Less

Submitted 5 June, 2024; originally announced June 2024.

Comments: Accepted at MFPS 2024

MSC Class: 03B45 (Primary); 03B20; 03B70; 68Q55; 06D20; 06D22; 06D05; 06D50; 18A15; 18A40; 18F20; 18D60; 18C10 (Secondary) ACM Class: F.4.1; F.3.2

Two-dimensional Kripke Semantics I: Presheaves

Authors: G. A. Kavvos

Abstract: The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond. The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond. △ Less

Submitted 8 May, 2024; v1 submitted 7 May, 2024; originally announced May 2024.

MSC Class: 03B45 (Primary); 03B20; 03B70; 68Q55; 06D20; 06D22; 06D10; 06D50; 18A15; 18A40; 18F20; 18D60 (Secondary) ACM Class: F.4.1; F.3.2

Journal ref: LIPIcs, Volume 299, FSCD 2024, article 11

Under Lock and Key: A Proof System for a Multimodal Logic

Authors: G. A. Kavvos, Daniel Gratzer

Abstract: We present a proof system for a multimodal logic, based on our previous work on a multimodal Martin-Loef type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e. a small 2-category. The logic is extended to a lambda calculus, establishing a Curry-Howard correspondence. We present a proof system for a multimodal logic, based on our previous work on a multimodal Martin-Loef type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e. a small 2-category. The logic is extended to a lambda calculus, establishing a Curry-Howard correspondence. △ Less

Submitted 18 May, 2023; v1 submitted 11 November, 2022; originally announced November 2022.

Comments: Version of Record to appear in the Bulletin of Symbolic Logic

Multimodal Dependent Type Theory

Authors: Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal

Abstract: We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quant… ▽ More We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion, thereby demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations. △ Less

Submitted 27 July, 2021; v1 submitted 30 November, 2020; originally announced November 2020.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 3 (July 28, 2021) lmcs:7571

Client-Server Sessions in Linear Logic

Authors: Zesen Qian, G. A. Kavvos, Lars Birkedal

Abstract: We introduce coexponentials, a new set of modalities for Classical Linear Logic. As duals to exponentials, the coexponentials codify a distributed form of the structural rules of weakening and contraction. This makes them a suitable logical device for encapsulating the pattern of a server receiving requests from an arbitrary number of clients on a single channel. Guided by this intuition we formul… ▽ More We introduce coexponentials, a new set of modalities for Classical Linear Logic. As duals to exponentials, the coexponentials codify a distributed form of the structural rules of weakening and contraction. This makes them a suitable logical device for encapsulating the pattern of a server receiving requests from an arbitrary number of clients on a single channel. Guided by this intuition we formulate a system of session types based on Classical Linear Logic with coexponentials, which is suited to modelling client-server interactions. We also present a session-typed functional programming language for server-client programming, which we translate to our system of coexponentials. △ Less

Submitted 3 March, 2021; v1 submitted 26 October, 2020; originally announced October 2020.

Recurrence Extraction for Functional Programs through Call-by-Push-Value (Extended Version)

Authors: G. A. Kavvos, Edward Morehouse, Daniel R. Licata, Norman Danner

Abstract: The main way of analyzing the complexity of a program is that of extracting and solving a recurrence that expresses its running time in terms of the size of its input. We develop a method that automatically extracts such recurrences from the syntax of higher-order recursive functional programs. The resulting recurrences, which are programs in a call-by-name language with recursion, explicitly comp… ▽ More The main way of analyzing the complexity of a program is that of extracting and solving a recurrence that expresses its running time in terms of the size of its input. We develop a method that automatically extracts such recurrences from the syntax of higher-order recursive functional programs. The resulting recurrences, which are programs in a call-by-name language with recursion, explicitly compute the running time in terms of the size of the input. In order to achieve this in a uniform way that covers both call-by-name and call-by-value evaluation strategies, we use Call-by-Push-Value (CBPV) as an intermediate language. Finally, we use domain theory to develop a denotational cost semantics for the resulting recurrences. △ Less

Submitted 11 November, 2019; originally announced November 2019.

Comments: POPL 2020

ACM Class: F.3.2

Journal ref: Proc. ACM Program. Lang. 4, POPL, Article 15 (January 2020)

Modalities, Cohesion, and Information Flow

Authors: G. A. Kavvos

Abstract: It is informally understood that the purpose of modal type constructors in programming calculi is to control the flow of information between types. In order to lend rigorous support to this idea, we study the category of classified sets, a variant of a denotational semantics for information flow proposed by Abadi et al. We use classified sets to prove multiple noninterference theorems for modaliti… ▽ More It is informally understood that the purpose of modal type constructors in programming calculi is to control the flow of information between types. In order to lend rigorous support to this idea, we study the category of classified sets, a variant of a denotational semantics for information flow proposed by Abadi et al. We use classified sets to prove multiple noninterference theorems for modalities of a monadic and comonadic flavour. The common machinery behind our theorems stems from the the fact that classified sets are a (weak) model of Lawvere's theory of axiomatic cohesion. In the process, we show how cohesion can be used for reasoning about multi-modal settings. This leads to the conclusion that cohesion is a particularly useful setting for the study of both information flow, but also modalities in type theory and programming languages at large. △ Less

Submitted 8 November, 2018; v1 submitted 20 September, 2018; originally announced September 2018.

Journal ref: G. A. Kavvos. 2019. Modalities, Cohesion, and Information Flow. Proc. ACM Program. Lang. 3, POPL, Article 20 (January 2019), 29 pages

On the Semantics of Intensionality and Intensional Recursion

Authors: G. A. Kavvos

Abstract: Intensionality is a phenomenon that occurs in logic and computation. In the most general sense, a function is intensional if it operates at a level finer than (extensional) equality. This is a familiar setting for computer scientists, who often study different programs or processes that are interchangeable, i.e. extensionally equal, even though they are not implemented in the same way, so intensio… ▽ More Intensionality is a phenomenon that occurs in logic and computation. In the most general sense, a function is intensional if it operates at a level finer than (extensional) equality. This is a familiar setting for computer scientists, who often study different programs or processes that are interchangeable, i.e. extensionally equal, even though they are not implemented in the same way, so intensionally distinct. Concomitant with intensionality is the phenomenon of intensional recursion, which refers to the ability of a program to have access to its own code. In computability theory, intensional recursion is enabled by Kleene's Second Recursion Theorem. This thesis is concerned with the crafting of a logical toolkit through which these phenomena can be studied. Our main contribution is a framework in which mathematical and computational constructions can be considered either extensionally, i.e. as abstract values, or intensionally, i.e. as fine-grained descriptions of their construction. Once this is achieved, it may be used to analyse intensional recursion. △ Less

Submitted 26 December, 2017; originally announced December 2017.

Comments: DPhil thesis, Department of Computer Science & St John's College, University of Oxford

MSC Class: 03B70; 03B45; 03F45; 68Q55; 18C50; 18A99 ACM Class: F.3.2; F.3.3; F.1.1; F.4.1; D.3.2; D.3.3

Intensionality, Intensional Recursion, and the Gödel-Löb axiom

Authors: G. A. Kavvos

Abstract: The use of a necessity modality in a typed $λ$-calculus can be used to separate it into two regions. These can be thought of as intensional vs. extensional data: data in the first region, the modal one, are available as code, and their description can be examined. In contrast, data in the second region are only available as values up to ordinary equality. This allows us to add non-functional opera… ▽ More The use of a necessity modality in a typed $λ$-calculus can be used to separate it into two regions. These can be thought of as intensional vs. extensional data: data in the first region, the modal one, are available as code, and their description can be examined. In contrast, data in the second region are only available as values up to ordinary equality. This allows us to add non-functional operations at modal types whilst maintaining consistency. In this setting, the Gödel-Löb axiom acquires a novel constructive reading: it affords the programmer the possibility of a very strong kind of recursion which enables them to write programs that have access to their own code. This is a type of computational reflection that is strongly reminiscent of Kleene's Second Recursion Theorem. △ Less

Submitted 13 June, 2020; v1 submitted 3 March, 2017; originally announced March 2017.

Comments: Presented at IMLA 2017. Revised version following post-conference review

The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time

Authors: G. A. Kavvos

Abstract: This is a survey of λ-calculi that, through the Curry-Howard isomorphism, correspond to constructive modal logics. We cover the prehistory of the subject and then concentrate on the developments that took place in the 1990s and early 2000s. We discuss logical aspects, modal λ-calculi, and their categorical semantics. The logics underlying the calculi surveyed are constructive versions of K, K4, S4… ▽ More This is a survey of λ-calculi that, through the Curry-Howard isomorphism, correspond to constructive modal logics. We cover the prehistory of the subject and then concentrate on the developments that took place in the 1990s and early 2000s. We discuss logical aspects, modal λ-calculi, and their categorical semantics. The logics underlying the calculi surveyed are constructive versions of K, K4, S4, and LTL. △ Less

Submitted 25 May, 2016; originally announced May 2016.

Kleene's Two Kinds of Recursion

Authors: G. A. Kavvos

Abstract: This is an elementary expository article regarding the application of Kleene's Recursion Theorems in making definitions by recursion. Whereas the Second Recursion Theorem (SRT) is applicable in a first-order setting, the First Recursion Theorem (FRT) requires a higher-order setting. In some cases both theorems are applicable, but one is stronger than the other: the FRT always produces least fixed… ▽ More This is an elementary expository article regarding the application of Kleene's Recursion Theorems in making definitions by recursion. Whereas the Second Recursion Theorem (SRT) is applicable in a first-order setting, the First Recursion Theorem (FRT) requires a higher-order setting. In some cases both theorems are applicable, but one is stronger than the other: the FRT always produces least fixed points, but this is not always the case with the SRT. Nevertheless, an old result by Rogers allows us to bridge this gap by subtly redefining the implementation of a higher-order functional in order to bring it to a `standard form.' △ Less

Submitted 4 August, 2018; v1 submitted 19 February, 2016; originally announced February 2016.

Comments: Contains slight errors. A corrected version can be found as Chapter 2 of DPhil thesis (arXiv:1712.09302)

Dual-Context Calculi for Modal Logic

Authors: G. A. Kavvos

Abstract: We present natural deduction systems and associated modal lambda calculi for the necessity fragments of the normal modal logics K, T, K4, GL and S4. These systems are in the dual-context style: they feature two distinct zones of assumptions, one of which can be thought as modal, and the other as intuitionistic. We show that these calculi have their roots in in sequent calculi. We then investigate… ▽ More We present natural deduction systems and associated modal lambda calculi for the necessity fragments of the normal modal logics K, T, K4, GL and S4. These systems are in the dual-context style: they feature two distinct zones of assumptions, one of which can be thought as modal, and the other as intuitionistic. We show that these calculi have their roots in in sequent calculi. We then investigate their metatheory, equip them with a confluent and strongly normalizing notion of reduction, and show that they coincide with the usual Hilbert systems up to provability. Finally, we investigate a categorical semantics which interprets the modality as a product-preserving functor. △ Less

Submitted 18 August, 2020; v1 submitted 15 February, 2016; originally announced February 2016.

Comments: Full version of article previously presented at LICS 2017 (see arXiv:1602.04860v4 or doi: 10.1109/LICS.2017.8005089)

ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 16, Issue 3 (August 19, 2020) lmcs:4740

On the Semantics of Intensionality

Authors: G. A. Kavvos

Abstract: In this paper we propose a categorical theory of intensionality. We first revisit the notion of intensionality, and discuss we its relevance to logic and computer science. It turns out that 1-category theory is not the most appropriate vehicle for studying the interplay of extension and intension. We are thus led to consider the P-categories of Čubrić, Dybjer and Scott, which are categories only u… ▽ More In this paper we propose a categorical theory of intensionality. We first revisit the notion of intensionality, and discuss we its relevance to logic and computer science. It turns out that 1-category theory is not the most appropriate vehicle for studying the interplay of extension and intension. We are thus led to consider the P-categories of Čubrić, Dybjer and Scott, which are categories only up to a partial equivalence relation (PER). In this setting, we introduce a new P-categorical construct, that of exposures. Exposures are very nearly functors, except that they do not preserve the PERs of the P-category. Inspired by the categorical semantics of modal logic, we begin to develop their theory. Our leading examples demonstrate that an exposure is an abstraction of well-behaved intensional devices, such as Gödel numberings. The outcome is a unifying framework in which classic results of Kleene, Gödel, Tarski and Rice find concise, clear formulations, and where each logical device or assumption involved in their proofs can be expressed in the same algebraic manner. △ Less

Submitted 25 April, 2017; v1 submitted 3 February, 2016; originally announced February 2016.

ACM Class: F.4.1

Journal ref: In: Esparza J., Murawski A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2017. Lecture Notes in Computer Science, vol 10203. Springer, Berlin, Heidelberg