Equivalence Proof for Intuitionistic Existential Alpha Graphs

AbstractLetSbe the group of finitely supported permutations of a countably infinite set. Let$K[S]$be the group algebra ofSover a fieldKof characteristic 0. According to a theorem of Formanek and Lawrence,$K[S]$satisfies the ascending chain condition for two-sided ideals. We study the reverse mathematics of this theorem, proving its equivalence over$RC{A_0}$(or even over$RCA_0^{\rm{*}}$) to the statement that${\omega ^\omega }$is well ordered. Our equivalence proof proceeds via the statement that the Young diagrams form a well partial ordering.

Download Full-text

Synchronous Message Passing and Semaphores: An Equivalence Proof

Abstract State Machines, Alloy, B and Z - Lecture Notes in Computer Science ◽

10.1007/978-3-642-11811-1_3 ◽

2010 ◽

pp. 20-33

Author(s):

Iain Craig ◽

Egon Börger

Keyword(s):

Message Passing ◽

Equivalence Proof

Download Full-text

The Equivalence Proof of Two Methods for Foundation Excitation

Applied Mechanics and Materials ◽

10.4028/www.scientific.net/amm.638-640.684 ◽

2014 ◽

Vol 638-640 ◽

pp. 684-689

Author(s):

Yun Ying Ma ◽

Jin Duan ◽

Hong Shao

Keyword(s):

Finite Element Analysis ◽

Finite Element ◽

Lagrange Multiplier ◽

Present Theory ◽

Degree Of Freedom ◽

Multiplier Method ◽

Element Analysis ◽

Numerical Example ◽

The Finite Element Analysis ◽

Equivalence Proof

In this paper, the two methods for the finite element analysis of foundation excitation would be proved mathematically equivalent. Although the two methods, i.e. the method of degree-of-freedom transformation and the Lagrange multiplier method, are absolutely different in appearance, but their mathematical essence would be proved completely identical. In other words, although the equations derived from the two methods have different degree-of-freedoms, i.e. the latter much more than the former, while in essence they could be deduced from each other and vice versa. And finally a numerical example will be presented and discussed to demonstrate the correctness of the present theory.

Download Full-text

Certifying derivation of state machines from coroutines

Proceedings of the ACM on Programming Languages ◽

10.1145/3498685 ◽

2022 ◽

Vol 6 (POPL) ◽

pp. 1-31

Author(s):

Mirai Ikebuchi ◽

Andres Erbsen ◽

Adam Chlipala

Keyword(s):

Data Structures ◽

Runtime Systems ◽

Web Browsers ◽

State Machines ◽

Implementation Challenges ◽

The Coq Proof Assistant ◽

Coq Proof Assistant ◽

Equivalence Proof ◽

High Level

One of the biggest implementation challenges in security-critical network protocols is nested state machines. In practice today, state machines are either implemented manually at a low level, risking bugs easily missed in audits; or are written using higher-level abstractions like threads, depending on runtime systems that may sacrifice performance or compatibility with the ABIs of important platforms (e.g., resource-constrained IoT systems). We present a compiler-based technique allowing the best of both worlds, coding protocols in a natural high-level form, using freer monads to represent nested coroutines , which are then compiled automatically to lower-level code with explicit state. In fact, our compiler is implemented as a tactic in the Coq proof assistant, structuring compilation as search for an equivalence proof for source and target programs. As such, it is straightforwardly (and soundly) extensible with new hints, for instance regarding new data structures that may be used for efficient lookup of coroutines. As a case study, we implemented a core of TLS sufficient for use with popular Web browsers, and our experiments show that the extracted Haskell code achieves reasonable performance.

Download Full-text