Concept

Linear logic

Related publications (16)

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based pro ...

Springer International Publishing Ag2024

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

2024

Working on mobility from people

Vincent Kaufmann

Describing, understanding, explaining and regulating mobility requires transversal approaches. Traditionally, mobility analysis proceeds by partitioning into four differentiated forms according to two dimensions: the temporality of which it is based and th ...

Routledge2021

Configuration logics: Modeling architecture styles

Joseph Sifakis, Simon Bliudze, Anastasia Mavridou, Eduard Baranov

We study a framework for the specification of architecture styles as families of architectures involving a common set of types of components and coordination mechanisms. The framework combines two logics: 1) interaction logics for the specification of arch ...

Elsevier Science Inc2017

A Semantic Framework for Architecture Modelling

Eduard Baranov

Architectures are common means for organising coordination between components in order to build complex systems and to make them manageable. They allow thinking on a higher plane and avoiding low-level mistakes. Architectures provide means for ensuring cor ...

EPFL2017

Parameterized Systems in BIP: Design and Model Checking

Joseph Sifakis, Simon Bliudze, Qiang Wang

BIP is a component-based framework for system design that has important industrial applications. BIP is built on three pillars: behavior, interaction, and priority. In this paper, we introduce first-order interaction logic (FOIL) that extends BIP to system ...

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik2016

Modelling Architecture Styles

Anastasia Mavridou

Software systems tend to increase over time in size and complexity. Their development usually spans a long period of time and often results in systems that are hard to understand, debug and maintain. Architectures are common means for organising coordinati ...

EPFL2016

Generalized Decision Rule Approximations for Stochastic Programming via Liftings

Daniel Kuhn, Wolfram Wiesemann

Stochastic programming provides a versatile framework for decision-making under uncertainty, but the resulting optimization problems can be computationally demanding. It has recently been shown that, primal and dual linear decision rule approximations can ...

Springer Verlag2015

Configuration Logics: Modelling Architecture Styles

Joseph Sifakis, Simon Bliudze, Anastasia Mavridou, Eduard Baranov

Springer Int Publishing Ag2015

Multiple Independent Gate FETs: How Many Gates Do We Need?

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Subhasish Mitra, Luca Gaetano Amarù

Multiple Independent Gate Field Effect Transistors (MIGFETs) are expected to push FET technology further into the semiconductor roadmap. In a MIGFET, supplementary gates either provide (i) enhanced conduction properties or (ii) more intelligent sw ...

IEEE2015

Closing the Gap between FPGA and ASIC : Balancing Flexibility and Efficiency

Hadi Parandeh Afshar

Despite many advantages of Field-Programmable Gate Arrays (FPGAs), they fail to take over the IC design market from Application-Specific Integrated Circuits (ASICs) for high-volume and even medium-volume applications, as FPGAs come with significant cost in ...

EPFL2012

Decision Procedures for Program Synthesis and Verification

Ruzica Piskac

Decision procedures are widely used in software development and verification. The goal of this dissertation is to increase the scope of properties that can be verified using decision procedures. To achieve this goal, we identify three improvements over the ...

EPFL2011

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Viktor Kuncak, Philippe Paul Henri Suter, Robin Steiger

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier- ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

Analyse non-linéaire des coques géodésiques multicouches à joints semi-rigides

Julius Natterer

In the 90ies the IBOIS-EPFL developed a new kind of shell structure. The ribs were made with simple boards waved together to form a spatial rib shell. However, the engineer currently does not have any effective method to calculate these kinds of spatial st ...

EPFL2010

Building a Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets ...

Springer2010

Convolution Operators And Homomorphisms Of Locally Compact Groups

Let 1 < p < infinity, let G and H be locally compact groups and let c) be a continuous homomorphism of G into H. We prove, if G is amenable, the existence of a linear contraction of the Banach algebra CVp (G) of the p-convolution operators on G into CVp (H ...

Cambridge University Press2008