We are hiring ! See our job offers.

sort by:
Revision Author Date Message Commit Date
f94b06d updated README 22 June 2021, 08:13:54 UTC
0a9345e Better pagination tokens 14 May 2020, 17:33:56 UTC
5963c0e Remove unnecessary map from paginationTokens 23 April 2020, 23:57:54 UTC
5a23fd2 F* done the F* way 23 April 2020, 23:35:22 UTC
d1c9de0 mapA for Tick applicative 22 April 2020, 19:24:37 UTC
cda4560 fix tests 16 March 2020, 20:43:43 UTC
8d287eb More mochi 02 March 2020, 23:01:12 UTC
a2b5559 Mochi tests in progress 02 March 2020, 07:42:11 UTC
e494a2f Updated fstar incr 02 March 2020, 07:41:39 UTC
d8391ff Adding fstar tests 26 February 2020, 02:54:16 UTC
9a832b4 oops 26 February 2020, 00:17:51 UTC
dc49dfd Added emptySet and intersection primOps 26 February 2020, 00:07:03 UTC
c915c9c mochi-d2 and mochi-d3 23 November 2019, 02:43:12 UTC
314ec0f app-succ and app-succ0 23 November 2019, 01:43:04 UTC
340b80e app-succ and repeat 23 November 2019, 01:29:11 UTC
f6db5fa Repeat is back 22 November 2019, 01:57:45 UTC
242582c mochi-d2 22 November 2019, 01:44:25 UTC
bea7946 Move mochi d2 to neg 22 November 2019, 01:44:25 UTC
347be3b added mochi tests 22 November 2019, 01:36:28 UTC
80cebdd Tick tick doesn't work 20 November 2019, 05:47:01 UTC
6f5b475 Omega isn't loop 20 November 2019, 05:37:09 UTC
093ff88 Tick tock 3: some real ticks and tocks 20 November 2019, 05:34:36 UTC
942eb2f Minor changes 20 November 2019, 03:19:40 UTC
0545284 add some of the tests from mochi 20 November 2019, 03:18:38 UTC
68d3acd Actual unbounded loop: DOES NOT WORK YET 19 November 2019, 07:26:18 UTC
2836ad7 Removed printing 19 November 2019, 05:36:34 UTC
9a417f5 Full looping for 19 November 2019, 01:47:25 UTC
91f9eff Automatically unpacking sigmas 19 November 2019, 00:35:44 UTC
0d76623 Wrote sigma-elaborator 18 November 2019, 21:46:22 UTC
fb48833 cleanup and hygiene 18 November 2019, 21:45:54 UTC
09636e9 Initial ANF sigma work 18 November 2019, 05:41:12 UTC
19db75a Fixed polymorphism bug 16 November 2019, 08:50:42 UTC
4350cd5 Switched to sigmas on some examples 16 November 2019, 07:00:22 UTC
7886cde Fixed freshRType bug 16 November 2019, 06:24:57 UTC
49bb9d0 Added RIFun to freshRType 13 November 2019, 19:56:36 UTC
5c0120a Pagination with tokens 13 November 2019, 19:56:36 UTC
301208f More interesting forSigma test 13 November 2019, 19:56:36 UTC
0b071dc Added implicit sigma types. Test and usage are in pos/forSigma.hs 13 November 2019, 19:56:36 UTC
ca8def0 Removed unneeded implicits 13 November 2019, 19:56:36 UTC
e0df534 Fixed typo in forSigma 13 November 2019, 19:56:36 UTC
3063e0e WIP on forSigma 13 November 2019, 19:56:36 UTC
66181ea Support for Higher-Rank Types you need double parens (see hrts.hs) 13 November 2019, 19:56:36 UTC
12b8e31 Pagination tokens 13 November 2019, 19:56:36 UTC
f791d87 Removing ANF 13 November 2019, 19:56:36 UTC
dca1c45 Commit before disabling ANF 13 November 2019, 19:56:36 UTC
ecf9dd9 Removed strengthening 13 November 2019, 19:56:36 UTC
d6c8677 Add partial pagination3 08 November 2019, 23:20:40 UTC
b52fffe Updated pure in tests 01 November 2019, 18:17:40 UTC
883df18 CPS script 29 October 2019, 22:35:08 UTC
082f610 Refixed parser 22 October 2019, 21:56:49 UTC
a90a8af More tests 22 October 2019, 21:46:04 UTC
f59c0b0 Merge commit of some sort 22 October 2019, 21:46:04 UTC
e7cedf6 shillSet experiments 22 October 2019, 21:46:04 UTC
5f94d69 added TCP client example 21 October 2019, 18:07:18 UTC
f9d43a2 run tests with setVerbosity Quiet 20 October 2019, 06:22:20 UTC
23ef471 Update to ticktock3 Add send/recv channels and prove that unreachable states are unreachable 18 October 2019, 19:01:34 UTC
c56ef6c Added twoPhaseCommit 17 October 2019, 21:33:07 UTC
ce240b3 added ticktock and pagination 17 October 2019, 02:31:23 UTC
f1d86f3 Read verbosity from command line instead of statically specifying it 17 October 2019, 02:31:23 UTC
3050d85 Added or and implication 14 October 2019, 18:56:59 UTC
a139996 idr_login finally works! 11 October 2019, 00:38:30 UTC
5570953 edits to idr_login 20 September 2019, 20:16:26 UTC
6aae376 Added implicit lambda term former 12 September 2019, 21:35:20 UTC
8ca0371 More work on idr examples - login example runs into strange bug in Checker articulation - intro example works, but need to make all types to Int to make FP happy 12 September 2019, 20:30:00 UTC
5c17971 Added test for renamer bug implicit args are in scope in the body in cgen, which is correct, but not in the renamer 10 September 2019, 18:29:33 UTC
6787ad4 First go at some real error messages Currently we print the bare refinement post-uniqify and freshening, but without the kvar sols having been applied, so that could definitely be improved upon 10 September 2019, 06:58:30 UTC
cd20f0c Fixed for.hs todo test. Needed to pull loop invariant into constraint on implicit parameter of callback. 09 September 2019, 21:24:19 UTC
1a405c6 Added todo/for case with refinement on iter index 09 September 2019, 20:12:25 UTC
9d7c337 - Fixed subtyping for constructors in Checker. - Made existential instantiation more robust. 29 August 2019, 18:36:54 UTC
c9b4d70 Fixed set annotations in shillSet 26 August 2019, 22:42:02 UTC
5ea1864 Fixed parsing of annotated lets and added negative test 26 August 2019, 20:40:22 UTC
ad522c2 Annotated let binders 21 August 2019, 03:43:02 UTC
22dbb0e correctly serialize type constructors to FP 21 August 2019, 01:06:17 UTC
579b1dc Better parse errors 19 August 2019, 09:38:42 UTC
a62e4b2 Update to lts-14.0 includes megaparsec 6 -> 7 migration, which changes the API for error messages and source positions also update fixpoint to to be on same lts 19 August 2019, 08:45:23 UTC
71eb919 Better formatted error messages from solver failures 15 August 2019, 23:20:00 UTC
b681213 Fixed printf format string 15 August 2019, 23:08:18 UTC
c3df68d Fixed Set bug 15 August 2019, 23:03:10 UTC
68df304 refactored SSParsedExpr 15 August 2019, 22:46:36 UTC
95861d2 SSParsedExpr is now recursive This recursion should probably be done at the ParsedExpr level, but that's an involved refactoring 15 August 2019, 22:45:56 UTC
9d2a590 Fixed test framework to use new config object 15 August 2019, 22:40:46 UTC
065c068 Added read option to mist 15 August 2019, 22:33:50 UTC
7069a8e start work on idris login example 07 August 2019, 18:51:37 UTC
ea1aad5 cleanup pointers example 04 August 2019, 05:52:42 UTC
97f6408 fix bug with implicits after forall 04 August 2019, 05:52:10 UTC
0c3f096 oops 04 August 2019, 05:30:22 UTC
e2b69aa unit in pointers_noalias.hs 02 August 2019, 18:44:06 UTC
4d122d5 Make pattern matcher timeout go away in ToFixpoint 02 August 2019, 18:11:54 UTC
ff589c2 Add unit Type 02 August 2019, 17:58:48 UTC
088d2fc Improve debugging output from CGen.hs 02 August 2019, 17:49:19 UTC
82249de Fix equal primOp 02 August 2019, 07:44:51 UTC
72aa198 isolated tabs/ifun bug and split into own test The problem is that when we have an ~> under an forall, at the term level we have a tabs, and that means we have to swtich from checking (at the type with the implicit parameter) to synthing (plus a subtyping check). But when we synth, this implicit parameter is simply not in scope: since it's not bound anywhere in the term, it can't be added to the context during synthesis. 01 August 2019, 07:53:00 UTC
95a7cd4 progress on state example: isolated bug some strage interaction between forall and implicits this causes forall a. h ~> n -> ... to get scoped as ``` forall n ... /\ forall h ... ``` instead of ``` forall n ... forall h .... ``` 30 July 2019, 18:46:43 UTC
0dc1fc4 Mixed up forall and rforall in CGen 30 July 2019, 18:40:47 UTC
3936ebc add subtyping rule fox right-hand implicits 29 July 2019, 15:15:06 UTC
4c79ff0 implement decr in pointers example. start init[ but seems there's a checker bug blocking init 29 July 2019, 05:25:06 UTC
bb8b279 added store primitive 29 July 2019, 04:54:52 UTC
60787e2 added map store 28 July 2019, 22:30:41 UTC
035e56a Set is a Ctor 24 July 2019, 11:45:36 UTC
d70ff51 split off todo/for.hs from shill 22 July 2019, 23:55:09 UTC
back to top