Commit Graph

  • 4362020a2b Final tweaks report regnat 2017-08-21 17:12:00 +0200
  • a5603de793 Simplify and inline the definition of derec regnat 2017-08-17 07:21:10 +0200
  • 72d5c75eb2 Use subscripts in compilation and semantics regnat 2017-08-17 07:18:41 +0200
  • 9235b7558c compilation: Add preprocessing of conditionals regnat 2017-08-17 07:10:56 +0200
  • 6b8ab05b73 Various minor changes regnat 2017-08-16 18:10:36 +0200
  • 212a5b0989 Fix examples regnat 2017-08-16 17:14:52 +0200
  • 5d840f02fb Fix the order of the figures regnat 2017-08-16 17:13:46 +0200
  • 2325ce9959 First draft of the conclusion regnat 2017-08-14 12:35:17 +0200
  • 1f3f834831 typing/records: quickly explain of the access rules regnat 2017-08-14 11:31:23 +0200
  • d4a2982d8a Add real code examples regnat 2017-08-14 11:26:11 +0200
  • 4363ee21a4 Fix compilation errors regnat 2017-08-14 10:52:39 +0200
  • 38fa84dc4d Move figures to the appendix regnat 2017-08-14 10:26:44 +0200
  • 360daadbee implem/extensions: apply Beppe's comments regnat 2017-08-14 10:21:18 +0200
  • bd4b4a8390 implem/modifications: apply Beppe's comments regnat 2017-08-14 10:15:19 +0200
  • 88a18f851a implem/cduce: apply Beppe's comments regnat 2017-08-14 10:13:15 +0200
  • 9a9441cf8a typing/about-soundness: apply Beppe's comments regnat 2017-08-14 10:11:37 +0200
  • f60a4f2327 typing/records: apply Beppe's comments regnat 2017-08-14 10:07:37 +0200
  • 828383932f typing/lists: apply Beppe's comments regnat 2017-08-14 09:42:04 +0200
  • c9e145bd83 typing/lambda-calculus: apply Beppe's comments regnat 2017-08-14 08:33:06 +0200
  • b1d2279300 typing/types: apply Beppe's comments regnat 2017-08-14 07:56:49 +0200
  • e0ffd542a2 nix-light/compilation: apply Beppe's comments regnat 2017-08-14 07:40:19 +0200
  • 8ce7da8d55 nix-light/description: apply Beppe's comments regnat 2017-08-14 07:14:36 +0200
  • 6b27b9f68f nix-light/motivation: apply Beppe's comments regnat 2017-08-13 19:54:16 +0200
  • 3fb0e15d65 set-theoretic-types: apply Beppe's comments regnat 2017-08-13 19:45:27 +0200
  • 234483ec44 nix/syntax-and-semantics: Apply Beppe's comments regnat 2017-08-13 19:37:08 +0200
  • 6ec7de1c13 Nix/general-presentation: apply Beppe's comments regnat 2017-08-13 16:03:17 +0200
  • 81a8072d99 outline: apply Beppe's review regnat 2017-08-13 15:49:22 +0200
  • 93ab3b3d5a synthesis: apply Beppe's comments regnat 2017-08-13 15:47:22 +0200
  • e1f745927d implem/lazy-subtyping: move definition to appendix regnat 2017-08-08 11:23:56 +0200
  • 623ab2b21a typing/records: add typing of record patterns regnat 2017-08-06 17:20:25 +0200
  • bfff67ca9d typing: Change appearance of the \accept operator regnat 2017-08-06 16:56:40 +0200
  • fa28b75c5b nix-light/description: record labels must be unique regnat 2017-08-06 16:02:20 +0200
  • 536efb76d4 Implem/extensions: add tracking of type predicates regnat 2017-08-06 15:55:50 +0200
  • 65b3b20e60 Remove obsolete TODO regnat 2017-08-06 15:22:27 +0200
  • c6f9c558ae Define the compilation of records regnat 2017-08-06 15:17:15 +0200
  • 462e505042 Add the needed fonts in the Nix environment regnat 2017-08-05 12:02:18 +0200
  • 66af8013f3 Define the compilation of recursive records regnat 2017-08-04 11:40:22 +0200
  • 953c72f4a6 Move Nix-light grammar to the appendix regnat 2017-08-04 11:22:14 +0200
  • 36a841cde3 Fix the grammar for values regnat 2017-08-04 11:01:20 +0200
  • 50dba02e5d Fix listing keywords font regnat 2017-08-04 10:59:59 +0200
  • 0e70ba9021 Replace french caption regnat 2017-08-04 10:40:07 +0200
  • ef029f388c let-rule: rewrite using the \overline notation regnat 2017-08-04 10:38:44 +0200
  • c114f87e72 pattern-matching semantic: simplify regnat 2017-08-04 10:02:48 +0200
  • 7f09712327 Change fonts regnat 2017-08-04 09:41:09 +0200
  • 2fea14fe70 nix/general-presentation: small rewordings regnat 2017-08-04 07:45:02 +0200
  • 227f095a9d synthesis: tweaks regnat 2017-08-04 07:33:46 +0200
  • 3da687b1d2 Shrink margins regnat 2017-08-03 17:20:15 +0200
  • dc8239e9a6 Adapt to the synthesis model imposed by the MPRI regnat 2017-08-03 17:19:33 +0200
  • 9e7e411815 extensions: small rewording regnat 2017-08-03 14:34:00 +0200
  • 093fe28c31 typing/records: small clarification regnat 2017-08-03 11:50:02 +0200
  • 1d6014fe42 implem/extensions: add part about special ops regnat 2017-08-03 11:46:45 +0200
  • 131fceeb62 implem/modifications: Replace by a talk about grad regnat 2017-08-03 11:46:30 +0200
  • 8cae9b8451 soundness: Tell that this is not our goal regnat 2017-08-03 10:15:28 +0200
  • b7b1f0b8af records: Fix the description of the rules regnat 2017-08-03 10:07:22 +0200
  • ea508a47a9 record: Fix the access rules regnat 2017-08-03 09:42:37 +0200
  • 070d20d8a5 records: Move to n-ary records regnat 2017-08-03 09:21:18 +0200
  • 6cb60d97a3 typing/lists: apply Beppe's review regnat 2017-08-02 12:11:57 +0200
  • 9277f7290a typing/lambda-calculus: apply Beppe's review regnat 2017-08-02 12:07:52 +0200
  • 56134751a4 Fix i.e. occurences regnat 2017-08-02 11:36:52 +0200
  • f5c5522130 typing/types: apply Beppe's review regnat 2017-08-02 11:32:29 +0200
  • ae89cdbd07 nix-light/compilation: apply Beppe's review regnat 2017-08-02 11:28:26 +0200
  • 1100d378bf nix-light/description: apply Beppe's review regnat 2017-08-02 10:28:53 +0200
  • 08e7cc20d6 nix-light/description: apply Beppe's review regnat 2017-08-02 09:59:04 +0200
  • 0dfd143a4d nix-light/motivation: apply Beppe's review regnat 2017-08-02 09:39:16 +0200
  • d6bd3ca9e4 Nix syntax: move to the appendix regnat 2017-08-02 09:27:37 +0200
  • 34ddb2e2ec nix/grammar: Emphase new constructs and split regnat 2017-08-02 09:09:24 +0200
  • 0d447d8caf context/set-theoretic-types: apply Bepee's review regnat 2017-08-02 08:36:15 +0200
  • 0d116398d3 nix/syntax-and-semantic: apply Beppe's review regnat 2017-08-02 08:27:27 +0200
  • 7d015b3a1a nix/general-presentation: Apply Beppe's review regnat 2017-08-02 08:17:37 +0200
  • 4ecbb4ec0e \pref -> \Cref regnat 2017-08-02 07:59:56 +0200
  • b90d93b06a Remove polyglossia regnat 2017-08-02 07:58:18 +0200
  • 2b0a2de598 contributions: Complete Beppe's draft regnat 2017-08-02 07:57:50 +0200
  • 427c8375be outline: rework regnat 2017-07-19 23:14:33 +0200
  • 3667b63aea nix/syntax-and-semantics: minor reformulations regnat 2017-07-19 15:00:24 +0200
  • 157dd374b3 nix/syntax: Briefly present the types regnat 2017-07-19 14:53:00 +0200
  • 92e20064d0 context/nix/general-presentation: shrink regnat 2017-07-19 14:38:27 +0200
  • 7483d12c87 typing/lambda-calculus: replace label by ref regnat 2017-07-19 14:34:20 +0200
  • ef87d82ebf Add outline regnat 2017-07-19 13:59:12 +0200
  • d856381e05 Change first Section outline regnat 2017-07-19 13:57:23 +0200
  • 3476829345 typos Beppe 2017-07-19 15:25:26 +0200
  • 6a1ed60b9b draft of contributions Beppe 2017-07-19 15:13:22 +0200
  • ab6d99748f Add contributions part regnat 2017-07-19 13:27:34 +0200
  • 7f2b6cb2f5 references: Small fixes regnat 2017-07-19 11:34:28 +0200
  • e6b2b6c4b7 Add release.nix regnat 2017-07-18 17:50:15 +0200
  • 638102ccd6 Use unicode for greek letters regnat 2017-07-18 17:49:21 +0200
  • 5e2e7f1b41 lualatex -> xelatex regnat 2017-07-18 17:43:28 +0200
  • 0fa568d21b implem/extensions: fix the semantic of import regnat 2017-07-18 10:06:04 +0200
  • f0e156d92a nix-light/grammar: Don' make Nil a base type regnat 2017-07-18 09:16:48 +0200
  • 67256cc8ea nix-light/grammar: reordonate regnat 2017-07-18 09:15:53 +0200
  • ed9430299d nix-ligh/grammar: add grammar for values regnat 2017-07-18 09:13:12 +0200
  • 0ed20cb8f3 nix-light/grammar: Fix record types in typecase regnat 2017-07-18 09:07:06 +0200
  • df179f7bfa nix-light/grammar: restrict the typecase regnat 2017-07-18 08:55:51 +0200
  • 3de9ae9da5 context/nix/general-presentation: translate regnat 2017-07-17 18:49:48 +0200
  • da9cec513d implem/extensions: Add even more stuff regnat 2017-07-17 16:53:55 +0200
  • 82256bcb68 implem/extensions: add more stuff regnat 2017-07-17 16:35:27 +0200
  • a72e832f8e nix/syntax: explicit that we just use a subset regnat 2017-07-17 16:13:28 +0200
  • 1344285981 implem/extensions: add stuff regnat 2017-07-17 16:13:01 +0200
  • e6bbff0f7e implem/modifications: don't over-hierarchise regnat 2017-07-17 16:12:16 +0200
  • bb2671d0e0 nix-light/grammar: add operators regnat 2017-07-17 15:46:25 +0200
  • a1cc785e9e nix-light: Remove access-paths regnat 2017-07-17 15:12:13 +0200