https://gitlab.com/nomadic-labs/mi-cho-coq

sort by:
Revision Author Date Message Commit Date
9fa0d6f OTT now compiles 14 March 2019, 16:10:12 UTC
db90922 Ignore generated files 14 March 2019, 15:43:01 UTC
a4724fa forgotten files ter 13 March 2019, 15:05:26 UTC
45c16a2 Forgotten files bis 13 March 2019, 14:57:39 UTC
4ce2c92 Forgotten files 13 March 2019, 14:55:50 UTC
10a4566 Mega refactoring + loosy integration of michocott 13 March 2019, 14:03:54 UTC
58fc6e7 Adding _CoqProject files and extraction 12 March 2019, 15:21:44 UTC
0888b30 Update the documentation 12 March 2019, 14:36:45 UTC
7fda535 DONE 12 March 2019, 14:36:45 UTC
6a39e09 New todos 12 March 2019, 14:36:45 UTC
eb4ac9a DONE 12 March 2019, 14:36:45 UTC
b660fc5 Rename "node" into "protocol environment" 12 March 2019, 14:36:45 UTC
c526321 Remove a useless abstract function 12 March 2019, 14:36:45 UTC
0b54305 Update TODO list 12 March 2019, 14:36:45 UTC
7cd504a All the functions provided by the environment are now expected to succeed 12 March 2019, 14:36:45 UTC
da384ba The self function from the environment cannot fail 12 March 2019, 14:36:45 UTC
3570b0d Add concrete syntax for lists In Michelson, the concrete syntax for lists is exactly the same as for sets excepts that the elements of sets must be given in ascending order. 12 March 2019, 14:36:45 UTC
8e6e8a8 Update the list of possible errors in the documentation 12 March 2019, 14:36:45 UTC
71ad127 Add a TODO list 12 March 2019, 14:36:45 UTC
6b5db67 Small simplification of the multisig specification 12 March 2019, 14:36:45 UTC
adf4cf5 Reorder the src/contracts directory 12 March 2019, 14:36:45 UTC
4fe2dbb Proof of correctness of the multisig contract 12 March 2019, 14:36:44 UTC
268bcd3 Compute a formula equivalent to precond (eval …) 12 March 2019, 14:36:44 UTC
8624d24 Prove evaluator’s monotonicity 12 March 2019, 14:36:44 UTC
b736184 Refactoring: fully separate syntax and semantics 12 March 2019, 14:36:44 UTC
070db99 More comparison lemmas 12 March 2019, 14:36:44 UTC
764ae68 Update the notations for sequences ";;" is now right associative to help reasoning on contracts in the forward direction. ";;;" does not show up in printing (it is too verbose). 12 March 2019, 14:36:44 UTC
8f407cc Add an example of a contract: multisig 12 March 2019, 14:36:44 UTC
8dfca2a Define most Michelson macros 12 March 2019, 14:36:44 UTC
1463e31 Generalize the types of the IF_* instructions. The documentation is buggy on this point; see https://gitlab.com/tezos/tezos/issues/471 12 March 2019, 14:36:44 UTC
4090095 Fix typing of FAILWITH FAILWITH takes no parameter but takes it argument on the stack. 12 March 2019, 14:36:44 UTC
ad253b1 Add a NOOP instruction doing nothing (written {} in Micheline) 12 March 2019, 14:36:44 UTC
c1509d2 Update typing of the CHECK_SIGNATURE instruction 12 March 2019, 14:36:44 UTC
023bda5 Rename a variable named I to avoid a name clash with the constructor of True 12 March 2019, 14:36:44 UTC
31288c7 Also remove obsolete instructions from the evaluator 12 March 2019, 14:36:44 UTC
39f508f Slides update 12 March 2019, 14:36:44 UTC
727ea56 Sort instructions by the order in which they are documented 12 March 2019, 14:36:44 UTC
6f93bf4 Remove obsolete instructions 12 March 2019, 14:36:44 UTC
76a7425 Add some comments 12 March 2019, 14:36:44 UTC
0911651 [README] Style 12 March 2019, 14:36:44 UTC
7fde4f5 Add some documentation 12 March 2019, 14:36:44 UTC
9e2186a Add the slides of today's presentation 12 March 2019, 14:36:44 UTC
ff33b5c Move code to the src directory 12 March 2019, 14:36:44 UTC
58dc95c Add LICENSE 12 March 2019, 14:36:44 UTC
fa36f83 Update to current status of Michelson 12 March 2019, 14:36:44 UTC
b2146ef Trailing whitespace 12 March 2019, 14:36:44 UTC
6e946a3 Syntax, typing, and operational semantics of the Michelson language in Coq 12 March 2019, 14:36:44 UTC
3e98c08 Initial commit 12 March 2019, 13:33:01 UTC
back to top