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

sort by:
Revision Author Date Message Commit Date
c631a79 [oracle_insurance|paper] add specification 20 May 2019, 09:16:21 UTC
bab9174 rm multisig modification 08 April 2019, 15:22:38 UTC
48ebec4 add work about modification of multisig 08 April 2019, 14:55:29 UTC
e2e399c [CI] Continuous integration The CI script does the following: - lint the `configure` shell scripts using `shellcheck` - lint the file `README.org` using `org-lint` - compile the project with Coq v8.8 and Coq v8.9. 03 April 2019, 14:03:44 UTC
baa2a13 [multisig] Replace `injection; discriminate` by `discriminate`. Some versions of Coq fail at useless calls to `injection`. 03 April 2019, 14:01:28 UTC
9019629 [build] By default, do not build the documentation 03 April 2019, 14:00:31 UTC
029eead [Build] Drop support for Coq < 8.8 03 April 2019, 13:56:13 UTC
0b1a985 [build] Ignore shellcheck false alarms 03 April 2019, 13:54:29 UTC
4f5d906 [License] Add License headers to all files 03 April 2019, 13:49:51 UTC
a9a08d3 [License] Assign copyright to Nomadic Labs 03 April 2019, 13:45:54 UTC
750f2f7 Make `./configure` work on more platforms Many OSes don't have `bash` in `/bin`, and in this case the script can be easily be made POSIX-compatible (hence `/bin/sh`). 22 March 2019, 18:17:46 UTC
03bd75c [Contracts] Adding Mutually calling contracts 18 March 2019, 14:24:05 UTC
709185b [Doc]Delete README.md in favor of README.org 18 March 2019, 14:24:05 UTC
89edb55 [Doc]Add installation instructions in the README 18 March 2019, 14:24:05 UTC
cc9a0ee [Build]Add an opam file 18 March 2019, 14:23:40 UTC
a1d6daa [License] Change (GPLv3 -> MIT) 18 March 2019, 14:23:40 UTC
515a6a2 [Doc][Coq][Contracts][Build]Refactoring - add _CoqProject + integration of michocott 18 March 2019, 14:23:32 UTC
0991155 [Doc]Update the documentation 15 March 2019, 15:38:57 UTC
1701b9c Update TODO list 15 March 2019, 14:47:54 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