20 citations · 54 across the 9 of their papers we have counts for
9 papers
Two-dimensional Kripke Semantics II: Stability and Completeness
G. A. Kavvos
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,…
Two-dimensional Kripke Semantics I: Presheaves
G. A. Kavvos
The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory…
Recurrence Extraction for Functional Programs through Call-by-Push-Value (Extended Version)
G. A. Kavvos, Edward Morehouse, Daniel R. Licata +1
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…
Modalities, Cohesion, and Information Flow
G. A. Kavvos
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 suppor…
On the Semantics of Intensionality and Intensional Recursion
G. A. Kavvos
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) equalit…
Intensionality, Intensional Recursion, and the Gödel-Löb axiom
G. A. Kavvos
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…
The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time
G. A. Kavvos
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 th…
Kleene's Two Kinds of Recursion
G. A. Kavvos
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…
On the Semantics of Intensionality
G. A. Kavvos
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…