23:46 Changeset [16351] by hritcu
23:25 Ticket #59 (Support security despite compromise) closed by hritcu
23:24 Ticket #59 (Support security despite compromise) created by hritcu
We now use intersection, union and refinement types; we have a sound and …
23:19 Ticket #58 (Wrong conversion of statements for FOL formulas) created by hritcu
The current conversion from statements to spass formulas does not take the …
23:04 Ticket #57 (Raise exceptions instead of returning false) created by hritcu
typeterm.ml uses exceptions to signal failure early (good), however …
22:53 Ticket #56 (Change everything to the FOL syntax defined in fol.ml) created by hritcu
We should still use the spass syntax inside the spass parser, but then we …
22:50 Ticket #55 (Move completely to sets) created by hritcu
No longer represent sets as lists. Get rid of "list2set" (performance …
22:48 Ticket #54 (Move to the new definition of environment extraction (using the logic)) created by hritcu
22:35 WikiStart edited by hritcu
22:34 WikiStart edited by hritcu
22:29 Changeset [16349] by hritcu
Polished statement verification
21:18 Ticket #50 (Fatal error: exception Stack_overflow) closed by hritcu
fixed: Doesn't occur any more
21:11 Changeset [16347] by hritcu
Strengthened the subtyping relation
15:42 Changeset [16345] by hritcu
Greatly improved statement verification: dealing with all cases and doing …
09:03 Changeset [16343] by hritcu
Improved naming of functions in parser.mly (Ticket #52)
09:00 Ticket #53 (Organize functions better in files and improve naming of files) created by hritcu
For instance: * term_to_stmt shouln't be located in print.ml * …
08:47 Ticket #52 (Improve naming of functions and keep naming consistent) created by hritcu
For instance: * We now have functions named 123, 321, foo, cfy etc. * …
08:29 Ticket #4 (Chose an official name for the type-checker) closed by hritcu
08:21 Changeset [16342] by hritcu
Slightly changed implementation of Proc-Des so that less type annotations …


21:23 Changeset [16337] by hritcu
Removed unnecessary configs from Makefile
20:47 Changeset [16335] by hritcu
Updated configs, and removed unnecessary ones
19:47 WikiStart edited by hritcu
19:37 Changeset [16331] by hritcu
Reimplemented statement verification (compile.ml). Now all sample …
14:38 Ticket #48 (Subtyping implementation very incomplete) closed by hritcu
13:48 Changeset [16328] by hritcu
Fixed bug in printing let processes
13:44 Changeset [16327] by hritcu
Done fixing examples
13:18 Changeset [16326] by hritcu
Fixed the last bug affecting daa.spi
12:44 Changeset [16324] by hritcu
Fixed many examples
11:49 Changeset [16323] by hritcu
Fixed the way tuples are dealt with (ftrue instead of true)
11:39 Changeset [16322] by broeni
changed form creation to create ftrue instead of S_True, adde special …
11:02 Changeset [16321] by broeni
maybe constructors should be printed as ftrue, like we defined it in the …
09:18 Changeset [16319] by hritcu
Fixed bug in rename_type for TRefine.
08:57 Changeset [16317] by hritcu
Updating the part of daa.spi related to blind signatures.
08:44 Changeset [16316] by hritcu
Made blind-sign.spi work by adding one type annotation.
08:32 Changeset [16315] by hritcu
Added new functions for checking equality between types and between spass …


22:30 Changeset [16311] by hritcu
Made term typing also use the very strong Refine rule
21:17 Changeset [16310] by hritcu
Removed seemingly spurious exception in spassprint.ml
20:51 Changeset [16309] by hritcu
Fixed bug in replace_stmt_in_formula
20:08 Changeset [16308] by hritcu
Got rid of the last traces of the ok token.
19:19 Changeset [16307] by hritcu
Updated forms so that it also extracts types from and and or types.
18:11 Changeset [16306] by broeni
added an unary symbol ftrue to the spass template and made the fol thing …
17:41 Changeset [16304] by broeni
fixed the list_fold2 exception for daa.spi and others by considering only …
14:12 Changeset [16296] by hritcu
Updated blind-sign.spi (still fails, but no longer because of syntax …
14:09 Changeset [16295] by broeni
some more try with statements around the fold_left2 statements
09:23 Changeset [16284] by broeni
got rid of debug code in environment well_formed by commenting out
09:21 Changeset [16283] by broeni
little debug change in spassprint undone
09:21 Changeset [16282] by broeni
changed create_form_from_sconstr that it NOW creates an S_Symbol(S_True) …


19:12 Changeset [16277] by broeni
added some debug output to environment to show the bug. This is ugly, but …
17:00 Changeset [16272] by hritcu
forgot to commit change to generator (done a while ago), sorry
17:00 Changeset [16271] by hritcu
simple.spi works for me now
16:07 Changeset [16270] by hritcu
Some first fixes (trying to make simple.spi work)
14:37 Changeset [16268] by hritcu
Made the pattern matchings more exhaustive
13:32 Changeset [16266] by hritcu
Made everything compile!
12:13 Changeset [16263] by hritcu
Temporarily removed compile.ml (to be added back, in rewritten form, where …
12:08 Changeset [16262] by hritcu
Made typeterm.ml compile. Many changes which need to be tried out in …
11:16 Changeset [16261] by hritcu
Got rid of "ok" tokens (replaced with "true" in the encoding of tuples)
09:41 Changeset [16260] by hritcu
Non-linear patterns now explicitly disallowed


19:11 Changeset [16248] by hritcu
Started to fix typeterm.ml (partial)
16:48 Changeset [16242] by hritcu
Added additional checks to kinding and subtyping.
16:39 Changeset [16241] by hritcu
Made unify.ml compile
16:10 Changeset [16239] by hritcu
updated ckind.ml so that it compiles
13:56 Changeset [16237] by broeni
think I got forms now right, except the renaming stuff. this is all …
12:52 WikiStart edited by hritcu
12:11 Changeset [16236] by hritcu
09:13 Changeset [16229] by hritcu
Rewritten kinding.ml and subtype.ml to use the new FOL syntax (still need …


21:18 Changeset [16223] by hritcu
New way to represent FOL formulas
20:35 Changeset [16221] by hritcu
20:32 Changeset [16220] by hritcu
Rewritten kinding.ml
20:00 Changeset [16219] by hritcu
Some small fixes to checker.ml


15:39 Changeset [16192] by tarrach


16:33 Ticket #13 (Get rid of ok, exercise, pair, etc.) closed by hritcu
15:08 Changeset [16167] by hritcu
Fixed the samples. They now ALL parse.
15:07 Changeset [16166] by hritcu
Fixed the samples. They now ALL parse.
15:06 Changeset [16165] by hritcu
Fixed the samples. They now ALL parse.
10:50 Changeset [16159] by hritcu
Now can parse refinement, and and or types.
10:27 Changeset [16158] by hritcu
Fixed the remaining old examples.
09:50 Changeset [16157] by hritcu
Fixed some of the old examples. Fixed parser so that we can parse them …
09:05 Changeset [16156] by hritcu
More small changes to syntax.
08:13 Changeset [16155] by hritcu
Fixed printing for refinement types.


21:08 Changeset [16153] by hritcu
Forgot a component of pair ... sorry ... fixed
18:41 Changeset [16147] by broeni
think I fixed replace and added a bound_spass function to alpha that has …
11:42 Changeset [16138] by broeni
environment should be fixed now. makes use of the new free method
11:13 Changeset [16137] by broeni
fixed the syntax things in functions. one open question remains
09:54 Changeset [16134] by hritcu
Removed useless stuff in spass template
09:48 Changeset [16133] by hritcu
Added pair splitting to parser.
09:41 Changeset [16132] by hritcu
Made get_fresh_name avoid a set of values (rather than a list)
09:27 Changeset [16131] by hritcu
Made the parser compile.
09:18 Changeset [16130] by hritcu
Removed some useless SPASS samples.


16:49 Changeset [16105] by hritcu
Started fixing the parser (partial)
16:14 Ticket #51 (Free should allow more than one identifier to be defined at a time) created by hritcu
15:39 Changeset [16100] by hritcu
15:26 Changeset [16099] by hritcu
Updated alpha.ml (partial)
11:55 Changeset [16094] by hritcu
New version of typechecker tailored to security despite compromise. …


17:30 WikiStart edited by hritcu
17:29 WikiStart edited by hritcu
17:26 WikiStart edited by hritcu
17:03 WikiStart edited by hritcu


13:02 Changeset [15919] by broeni
built the changes in check_e into check and modified main to accept a …
13:00 Changeset [15918] by broeni
removed the double check_e thing


19:43 Ticket #50 (Fatal error: exception Stack_overflow) created by hritcu
./typecheck -v 3 ~/Research/Students?/martin_grochulla/process_says.spi
14:29 Changeset [15911] by grochulla
checker.ml with eprove


22:56 Changeset [15910] by hritcu
The proof obligations that were immediately discharged were also added to …
21:52 Changeset [15908] by hritcu
Brand new implementation of kinding and subtyping (partial; new versions …
18:32 Ticket #47 (Problem Counting Proof Obligations?) closed by hritcu
18:30 Changeset [15904] by hritcu
The proof obligations that were immediately discharged were also added to …
17:26 Changeset [15903] by grochulla
additional options for eprover
14:31 Changeset [15900] by grochulla
added checker_e.ml file which invokes eprover instead of spass makeing …


13:22 Ticket #49 (Support timeouts for provers) created by hritcu
Most provers support timeouts as command line arguments. We could also …


13:35 Ticket #48 (Subtyping implementation very incomplete) created by hritcu
The current implementation of the subtyping relation is very incomplete. …
11:34 Changeset [15830] by hritcu
In martin2.config I removed all cases other than the one for check, and …


13:23 Changeset [15779] by hritcu
11:57 Changeset [15776] by hritcu
Fixed to match paper (using long term public key of the issuer to create …
10:51 Ticket #47 (Problem Counting Proof Obligations?) created by hritcu
Make sure that the numbers displayed while logging always match the ones …
10:35 Milestone 0.1.0 (CCS) completed
07:26 WikiHtml edited by trac
07:26 WikiMacros edited by trac
07:26 WikiNewPage edited by trac
07:26 WikiPageNames edited by trac
07:26 WikiProcessors edited by trac
07:26 WikiRestructuredTextLinks edited by trac
07:26 TracRss edited by trac
07:26 TracSearch edited by trac
07:26 TracStandalone edited by trac
07:26 TracSupport edited by trac
07:26 WikiDeletePage edited by trac
07:26 TracTickets edited by trac
07:26 TracTimeline edited by trac
07:26 TracWiki edited by trac
07:26 TracTicketsCustomFields edited by trac
07:26 TracUnicode edited by trac
07:26 TracUpgrade edited by trac
07:26 TracWorkflow created by trac
07:26 WikiRestructuredText edited by trac
07:26 WikiFormatting edited by trac
07:26 TracInstall edited by trac
07:26 TracLinks edited by trac
07:26 TracLogging edited by trac
07:26 TracInterfaceCustomization edited by trac
07:26 TracModPython edited by trac
07:26 TracModWSGI created by trac
07:26 TracNavigation created by trac
07:26 TracNotification edited by trac
07:26 TracPermissions edited by trac
07:26 TracPlugins edited by trac
07:26 TracQuery edited by trac
07:26 TracReports edited by trac
07:26 TracRevisionLog edited by trac
07:26 TracRoadmap edited by trac
07:26 TitleIndex edited by trac
07:26 TracChangeset edited by trac
07:26 TracAdmin edited by trac
07:26 TracBackup edited by trac
07:26 TracBrowser edited by trac
07:26 TracCgi edited by trac
07:26 TracSyntaxColoring edited by trac
07:26 TracEnvironment edited by trac
07:26 TracFastCgi edited by trac
07:26 TracGuide edited by trac
07:26 TracImport edited by trac
07:26 TracFineGrainedPermissions created by trac
07:26 TracIni edited by trac
07:26 PageTemplates created by trac
07:26 CamelCase edited by trac
07:26 InterTrac edited by trac
07:26 InterWiki edited by trac
07:26 TracAccessibility edited by trac
07:26 RecentChanges edited by trac


21:04 Changeset [15765] by hritcu
Added subtype_immediately function and made martin2.config use it
18:40 Changeset [15764] by grochulla
committing previous version of config-file
17:56 Changeset [15763] by grochulla
now implemented correctly
16:44 Changeset [15762] by hritcu
Added 2 of Martin's config that were referenced by the Makefile


13:43 Changeset [15726] by grochulla
added configuration file martin2.config and modified makefile
11:01 WikiStart edited by broeni
Note: See TracTimeline for information about the timeline view.