相关论文: Curry-style type Isomorphisms and Game Semantics

In this research summary we present our recent work on implementing functional patterns with inverse functions in the lazy functional-logic programming language Curry. Our goal is the synthesis of the inverse of any given function in Curry…

The present article is a brief informal survey of computability logic --- the game-semantically conceived formal theory of computational resources and tasks. This relatively young nonclassical logic is a conservative extension of classical…

In automated complexity analysis, noninterference-based type systems statically guarantee, via soundness, the property that well-typed programs compute functions of a given complexity class, e.g., the class FP of functions computable in…

We develop a method that integrates the tree of thoughts and multi-agent framework to enhance the capability of pre-trained language models in solving complex, unfamiliar games. The method decomposes game-solving into four incremental tasks…

This paper defines a sound and complete semantic criterion, based on reducibility candidates, for strong normalization of theories expressed in minimal deduction modulo \`a la Curry. The use of Curry-style proof-terms allows to build this…

Argumentation is one of the most popular approaches of defining a~non-monotonic formalism and several argumentation based semantics were proposed for defeasible logic programs. Recently, a new approach based on notions of conflict…

Game semantics is a denotational semantics presenting compositionally the computational behaviour of various kinds of effectful programs. One of its celebrated achievement is to have obtained full abstraction results for programming…

We propose a type-theoretic framework for describing and proving properties of quantum computations, in particular those presented as quantum circuits. Our proposal is based on an observation that, in the polymorphic type system of Coq,…

Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and concurrent calculi; it is governed by type systems that…

Reasoning is not just about solving problems -- it is also about evaluating which problems are worth solving at all. Evaluations of artificial intelligence (AI) systems primarily focused on problem solving, historically by studying how…

Cirquent calculus is a proof system manipulating circuit-style constructs rather than formulas. Using it, this article constructs a sound and complete axiomatization CL16 of the propositional fragment of computability logic (the…

We present an approach to modeling computational calculi using higher category theory. Specifically we present a fully abstract semantics for the pi-calculus. The interpretation is consistent with Curry-Howard, interpreting terms as typed…

Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classic versions of LL (ILL and CLL), we obtain two different…

Extensive games are tools largely used in economics to describe decision processes ofa community of agents. In this paper we propose a formal presentation based on theproof assistant COQ which focuses mostly on infinite extensive games and…

The class of algorithmically computable simple games (i) includes the class of games that have finite carriers and (ii) is included in the class of games that have finite winning coalitions. This paper characterizes computable games,…

Hierarchies of conditional beliefs (Battigalli and Siniscalchi 1999) play a central role for the epistemic analysis of solution concepts in sequential games. They are modelled by type structures, which allow the analyst to represent the…

A large body of research is currently investigating on the connection between machine learning and game theory. In this work, game theory notions are injected into a preference learning framework. Specifically, a preference learning problem…

A type system combining type application, constants as types, union types (associative, commutative and idempotent) and recursive types has recently been proposed for statically typing path polymorphism, the ability to define functions that…

We introduce Probabilistic Dependent Type Systems (PDTS) via a functional language based on a subsystem of intuitionistic type theory including dependent sums and products, which is expanded to include stochastic functions. We provide a…

Type refinements combine the compositionality of typechecking with the expressivity of program logics, offering a synergistic approach to program verification. In this paper we apply dependent type refinements to SAX, a futures-based…