These are chat archives for groupoid/exe

23rd
Feb 2017
Namdak Tonpa
@5HT
Feb 23 2017 01:56
вот оно
нашел
http://goto.ucsd.edu/reflex/
https://github.com/siegebell/vscoq — а это просто плагинчик к VS Code
вот такие скрипты чекает рефлекс https://github.com/UCSD-PL/kraken/blob/master/reflex/coq/bench-quark/Kernel.reflex
  When t:Tab sends CookieChannelInit(f) respond:
    lookup CProc(t.domain)
    { cp => send(cp, TabProcessRegister(f)) }
    { c <- spawn CProc(t.domain);
      send(c, DomainSet(t.domain));
      send(c, TabProcessRegister(f))
    }

Properties :
  CProcUnique:
    forall d:
      [Spawn CProc(d)] Disables [Spawn CProc(d)]

  CookieSameDomain:
    forall d, f:
      [Recv(Tab(_, d), CookieChannelInit(f))]
      Enables
      [Send(CProc(d), TabProcessRegister(f))]
Namdak Tonpa
@5HT
Feb 23 2017 02:05
In this section, we describe the REFLEX interpreter and the BehAbs function, which, given a program P, computes a behavioral ab- straction characterizing the traces P can produce. We emphasize design decisions following LAC that allow us to prove once and for all, manually in Coq, that the traces produced by running the interpreter on program P satisfy BehAbs(P ). We illustrate these REFLEX features at a high level, but the full, commented REFLEX implementation is available online.
REFLEX programs implement reactive systems, which are funda- mentally impure and non-terminating. To support these features in Coq’s otherwise pure, strongly normalizing core calculus, we wrote our interpreter using the Ynot [17] library for encoding monadic stateful computations in Coq. The REFLEX interpreter interacts with the outside world using Ynot to invoke effectful operations; each operation is guarded by low-level pre-conditions to ensure their proper use, e.g. sends may only be performed on open file de- scriptors. For example, at the bottom of Figure 4, we see the Ynot axiomatization of the send primitive which takes as input a chan- nel c and string s to write to c. Additionally send takes the current trace as an input.
чесно говоря эхо сервер Адама Чипалы меня не радует