FWIW, Jonathan Schuster's encoding of NetCore (the Princeton-Cornell theory for
routing, last popl) encountered a similar problem. The original paper uses the
ChemAM and he encoded it with Redex with "propagated parts of patterns".
So in general, models based on the Chem AM would be easier to
du
Sent: Wednesday, June 20, 2012 9:20:35 AM GMT -05:00 US/Canada Eastern
Subject: Re: [racket-dev] Redex for abstract machines / analysis prototypes
On Wed, Jun 20, 2012 at 7:48 AM, J. Ian Johnson wrote:
> My papers have been using record notation. Say for lookup:
> s{C = x, E = rho} --&
t think I said it wasn't.
Robby
> -Ian
> - Original Message -
> From: Robby Findler
> To: J. Ian Johnson
> Cc: dev , n...@ccs.neu.edu
> Sent: Wed, 20 Jun 2012 01:27:18 -0400 (EDT)
> Subject: Re: [racket-dev] Redex for abstract machines / analysis prototypes
>
>
EDT)
Subject: Re: [racket-dev] Redex for abstract machines / analysis prototypes
I have thought about adding something that would solve this problem to
Redex off and on for a few years and am circling something I think is
reasonable. (The main thing I think you've not considered below is how
to
I have thought about adding something that would solve this problem to
Redex off and on for a few years and am circling something I think is
reasonable. (The main thing I think you've not considered below is how
to typeset things, but that said I have in mind something similar in
spirit to what you
Machine semantics for real machines (like the JVM or Racket's VM) or
non-standard semantics for an abstract interpretation (like what I end up
getting into) can get up to monstrous numbers of components for each state that
usually don't matter. I and I'm sure many others would appreciate a reduc
6 matches
Mail list logo
