Publications related to 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

Additional Material for "Unifying Data Representation Transformations"

Vlad Ureche

This report shows an attempt to formalize the data representation transformation mechanism in the ``Unifying Data Representation Transformations'' paper. Since the mechanism described in the paper is targeted at the Scala programming language and the speci ...

2014

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

On Complete Completion using Types and Weights

Viktor Kuncak, Ruzica Piskac, Tihomir Gvero, Ivan Kuraj

Developing modern software applications 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 ...

2012

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

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

Dirk Thilo Beyer, Grégory Théoduloz

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

Normal form (abstract rewriting)

Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

Structural Rewriting in XOR-Majority Graphs

Higher-Order Subtyping with Type Intervals

Additional Material for "Unifying Data Representation Transformations"

Complete Completion using Types and Weights

Bifurcation Analysis at a Singular Soliton State in Fiber Couplers

On Complete Completion using Types and Weights

Opis: Reliable Distributed Systems in OCaml

Opis: Reliable Distributed Systems in OCaml

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

Graph Chatbot

Chat with Graph Search

Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

Structural Rewriting in XOR-Majority Graphs

Higher-Order Subtyping with Type Intervals

Additional Material for "Unifying Data Representation Transformations"

Bifurcation Analysis at a Singular Soliton State in Fiber Couplers

Complete Completion using Types and Weights

Opis: Reliable Distributed Systems in OCaml

On Complete Completion using Types and Weights

Opis: Reliable Distributed Systems in OCaml

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