[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Using TLA+ for Simulation-proofs

Hi all,

I'm just beginning to learn about TLA+ and trying to understand some of the capabilities it provides and the problems it could be used to solve.

I'm curious if TLA+ could be used for specifying simulation-proofs (e.g., https://eccc.weizmann.ac.il/report/2017/112/). 

I haven't seen much about such a use case discussed online. If it could be used for something like this, any pointers? I'm especially interested in computational indistinguishability in the real/ideal world paradigm.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7311211f-1c54-4225-8f2a-af18f3e2e57bn%40googlegroups.com.