Publications associées à Normal form (abstract rewriting)

Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

We present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of boolean algebra. We use as a base a variation of Hopcroft, Ullman and Aho algorithm for tree isomo ...

Springer2022

Structural Rewriting in XOR-Majority Graphs

Giovanni De Micheli, Mathias Soeken, Zhufei Chu

In this paper, we present a structural rewriting method for a recently proposed XOR-Majority graph (XMG), which has exclusive-OR (XOR), majority-of-three (MAJ), and inverters as primitives. XMGs are an extension of Majority-Inverter Graphs (MIGs). Previous ...

ASSOC COMPUTING MACHINERY2019

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

Complete Completion using Types and Weights

Viktor Kuncak, Ruzica Piskac, Tihomir Gvero, Ivan Kuraj

Developing modern software typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that synthesizes ...

ACM2013

Bifurcation Analysis at a Singular Soliton State in Fiber Couplers

Boris Buffoni

The system {-u '' + u = u(3) + lambda v, u(x)= u(-x) is an element of R, x is an element of R, -v '' + v = v(3) + lambda u, v(x) = v(-x) is an element of R, x is an element of R, describes pulses in nonlinear fiber couplers. It has the family (U1+lambda, - ...

Advanced Nonlinear Studies, Inc2012

Opis: Reliable Distributed Systems in OCaml

Dejan Kostic, Viktor Kuncak, Pierre-Evariste Dagand

Concurrency and distribution pose algorithmic and implementation challenges in developing reliable distributed systems, making the field an excellent testbed for evaluating programming language and verification paradigms. Several specialized domain-specifi ...

2009

Opis: Reliable Distributed Systems in OCaml

Viktor Kuncak, Dejan Kostic, Pierre-Evariste Dagand

Concurrency and distribution pose algorithmic and implementation challenges in developing reliable distributed systems, making the field an excellent testbed for evaluating programming language and verification paradigms. Several specialized domain-specifi ...

2009

Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis

Grégory Théoduloz, Dirk Thilo Beyer

In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this p ...

Springer2007

A typed intermediate language and algorithms for compiling scala by successive rewritings

Philippe Altherr

Scala is a general-purpose programming language developed at EPFL. It combines concepts coming from object-oriented languages with other ones coming from functional languages. Scala is strongly typed and comes with a relatively complex type system, which i ...

EPFL2006