Home

Formal semantics

Formal sciences
Theoretical computer science
Programming language theory
Formal semantics

About
Privacy
Disclaimer

Graph Chatbot

Related publications (22)

Measurement of the ratio of branching fractions of the decays0(2S) and arrange Lambda

Christoph Frei, Peter Clarke, Jean Wicht, Aurelio Bay, Minh Tâm Tran, Marc-Olivier Bettler, Cédric Potterat, François Fleuret, Tatsuya Nakada, Guido Haefeli, Niko Neufeld, Olivier Schneider, Hans Dijkstra, Frédéric Teubert, Gerhard Raven, Mingkui Wang, Chitsanu Khurewathanakul, Frédéric Blanc, Matthew Needham, Axel Kuonen, Olivier Göran Girard, Liang Sun, Maxime Schubiger, Thibaud Humair, Hang Yin, Xiaoxue Han, Luis Alberto Granado Cardoso, Greig Alan Cowan, Paolo Durante, Jessica Prisciandaro, Guillaume Max Pietrzyk, Matthieu Philippe Luther Marinangeli, Daniel Hugo Cámpora Pérez, Vladislav Balagura, Lino Ferreira Lopes, Zhirui Xu, Mark Tobin, Victor Coco, Violaine Bellée, Mirco Dorigo, , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , ,

The epsilon expansion meets semiclassics

Riccardo Rattazzi, Alexander Monin, Gil Badel, Gabriel Francisco Cuomo

We study the scaling dimension Delta(phi n) of the operator phi(n) where phi is the fundamental complex field of the U(1) model at the Wilson-Fisher fixed point in d = 4 - epsilon. Even for a perturbatively small fixed point coupling lambda*, standard pert ...

Springer Nature2019

Higher-Order Subtyping with Type Intervals

Sandro Stucki

Modern, statically typed programming languages provide various abstraction facilities at both the term- and type-level. Common abstraction mechanisms for types include parametric polymorphism -- a hallmark of functional languages -- and subtyping -- which ...

EPFL2017

Type Soundness Proofs with Definitional Interpreters

Nada Amin, Tiark Rompf

While type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (DOT) calculu ...

Assoc Computing Machinery2017

Simplicitly: Foundations and Applications of Implicit Function Types

Martin Odersky, Sandro Stucki, Olivier Eric Paul Blanvillain, Heather Christine Klug, Fengyun Liu

Understanding a program entails understanding its context; dependencies, configurations and even implementations are all forms of contexts. Modern programming languages and theorem provers offer an array of constructs to define contexts, implicitly. Scala ...

2017

Indicators of Evidence for Bioequivalence

Stephan Morgenthaler, Robert Staudte

Some equivalence tests are based on two one-sided tests, where in many applications the test statistics are approximately normal. We define and find evidence for equivalence in Z-tests and then one-and two-sample binomial tests as well as for t-tests. Mult ...

Mdpi Ag2016

Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP

Simon Bliudze, Eduard Baranov

Based on a concise but comprehensive overview of some fundamental properties required from component-based frameworks, namely compositionality, incrementality, flattening, modularity and expressiveness, we review three modifications of the semantics of glu ...

Elsevier2015

RSP-QL Semantics: a Unifying Query Model to Explain Heterogeneity of RDF Stream Processing Systems

Jean Paul Calbimonte Perez

RDF and SPARQL are established standards for data interchange and querying on the Web. While they have been shown to be useful and applicable in many scenarios, they are not sufficiently adequate for dealing with streams of data and their intrinsic continu ...

2014

Extended Connectors: Structuring Glue Operators in BIP

Simon Bliudze, Eduard Baranov

Based on a variation of the BIP operational semantics using the offer predicate introduced in our previous work, we extend the algebras used to model glue operators in BIP to encompass priorities. This extension uses the Algebra of Causal Interaction Trees ...

2013

Stochastic fragments: A framework for the exact reduction of the stochastic semantics of rule-based models

Tatjana Petrov

In this paper, we propose an abstract interpretation-based framework for reducing the state space of stochastic semantics for protein protein interaction networks. Our approach consists in quotienting the state space of networks. Yet interestingly, we do n ...

2013

Lumpability Abstractions of Rule-based Systems

Tatjana Petrov

The induction of a signaling pathway is characterized by transient complex formation and mutual posttranslational modification of proteins. To faithfully capture this combinatorial process in a mathematical model is an important challenge in systems biolog ...

2010

Decision Procedures for Algebraic Data Types with Abstractions

Mirco Dotta, Philippe Paul Henri Suter, Viktor Kuncak

We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term a ...

2010

Constraint Solving for Software Reliability and Text Analysis

Viktor Kuncak

We will develop and implement new algorithms for constraint solving and apply them to construct two classes of tools: 1) bug finding and verification tools building on tools such as Java PathFinder and Jahob; 2) tools for deep semantic analysis of texts co ...

2008

Semantics of OCL specified with QVT

Slavisa Markovic

The Object Constraint Language (OCL) has been for many years formalized both in its syntax and semantics in the language standard. While the official definition of OCL's syntax is already widely accepted and strictly supported by most OCL tools, there is n ...

Springer-Verlag2008

Equivalences and calculi for formal verification of cryptographic protocols

Johannes Borgström

Security protocols are essential to the proper functioning of any distributed system running over an insecure network but often have flaws that can be exploited even without breaking the cryptography. Formal cryptography, the assumption that the cryptograp ...

EPFL2008

Conceptual Synopses of Semantics in Social Networks Sharing Structured Data

We are interested in the problem of data sharing in overlay networks that have a social structure, i.e. participants are linked and exchange data with others w.r.t. the similarity of their data semantics. In this paper we propose a methodology to produce c ...

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

Formal Semantics for Property-Property Relations in SEAM Visual Language: Towards Simulation and Analysis of Visual Specifications

Alain Wegmann, Irina Rychkova

SEAM is an enterprise architecture method that defines a visual language for modeling. Our goal is to provide formal semantics for SEAM. Model simulation, model comparison, and refinement verification are practical benefits we expect from this formalizatio ...

2007

A formal semantics for protocol narrations

Sébastien Briais

Protocol narrations are a widely-used informal means to describe, in an idealistic manner, the functioning of cryptographic protocols as a single intended sequence of cryptographic message exchanges among the protocol’s participants. Protocol narrations ha ...

2007

Foundations for SCALA : semantics and proof of virtual types

Vincent Cremet

SCALA is an attractive programming language because it is both very expressive and statically strongly typed. This marriage against nature comes at the price of a certain complexity in the language constructs and the static analysis. This complexity makes ...

EPFL2006

An OCL Semantics Specified with QVT

Slavisa Markovic

Metamodeling became in the last decade a widely accepted tool to describe the (abstract) syntax of modeling languages in a concise, but yet precise way. For the description of the language's semantics, the situation is less satisfactory and formal semantic ...

2006

Page 1 of 2

Plamen Hristov Hopchev

Maria Elena Stramaglia

Aravindhan Venkateswaran

Luis Miguel Garcia Martin

Giovanni Carboni

Using pp collisions corresponding to 3 fb integrated luminosity, recorded by the LHCb experiment at centre- of- mass energies of 7 and 8TeV, the ratio of branching fractions B (0b ! (2 S) ) =B (0b ! J= ) = 0 : 513 0 : 023 (stat) 0 : 016 (syst) 0 : 011 (B) ...

Springer Nature2019