thufschmitt/tix-papers
1
1
Fork 0
mirror of https://github.com/thufschmitt/tix-papers.git synced 2024-09-11 13:00:34 +03:00
Code Issues Projects Releases Wiki Activity
164 Commits 8 Branches 0 Tags 1.2 MiB
lambda_calculus
Commit Graph

164 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
regnat
67b67be7c4 oracle: State and prove subject reduction 2017-05-23 07:36:19 +02:00
regnat
15c49c3cfc Define the "oracle" type-system 2017-05-23 07:34:10 +02:00
regnat
a78a2a3d60 Move "soundness" to its own part 2017-05-22 08:30:45 +02:00
regnat
3dd6b5ab03 Expand the explications of nix typing 2017-05-19 10:45:37 +02:00
regnat
08b2d4ba77 Rewrite the compilation of if using the D set 2017-05-19 09:29:23 +02:00
regnat
65f3140b27 Add typing rules for nix 2017-05-19 09:24:05 +02:00
regnat
dcf39d23d7 fixup! Add builtins functions to nix syntax 2017-05-19 09:00:55 +02:00
regnat
7dea85d439 Rephrase the presentation of nix-light semantics 2017-05-19 09:00:17 +02:00
regnat
2d32a8840b Add builtins functions to nix syntax 2017-05-19 08:20:29 +02:00
regnat
f9445db6bb Reorganize physical hierarchy 
Thi makes it closer to the structure of the document and much easier to
work with
 2017-05-19 08:01:25 +02:00
regnat
83fda3ddbf typing: replace bad pair example by better list one 
The pair example used a sub-optimal algorithm that didn't work except on
trivial cases.
The now one explicitly states that we only consider trivial cases.
 2017-05-18 11:29:28 +02:00
regnat
833bbb7946 Grammar: make Nil a constant 2017-05-18 11:29:28 +02:00
regnat
9f5ee29ace typing: add a rule for Cons 
The checking rule requires the annotation to be exactly in the form
Cons(τ₁, τ₂), because treating the general case would be too much of a
hassle.
 2017-05-18 11:27:50 +02:00
regnat
520b5127d6 State subject reduction for the check type system 
The proof is eluded as it is very similar to the one for the infer type
system
 2017-05-18 10:53:18 +02:00
regnat
11d1227b46 subj-reduct : add proof for the ITcase rule 
This completes the proof.

It is currently wrong, as we assert that for any closed value v and any
type t, ⊢ v :t or ⊢ v : ¬ t, which requires a modification in the
type-system to hold.
 2017-05-18 10:53:18 +02:00
regnat
6bdbed957f typing: merge TCase{L,R} rules into {C,I}CaseLR 
(and rename {C,I}CaseLR to {C,I}Case)
 2017-05-18 10:52:58 +02:00
regnat
e5f539263c subj-reduct: add non-proof for the letAnnot case 2017-05-18 10:52:36 +02:00
regnat
ec401b8d70 subj-reduct: add proof of the Let case 2017-05-18 10:52:29 +02:00
regnat
92735099d1 Add the begining of the proof of subject reduction 2017-05-17 18:22:30 +02:00
regnat
a50d058476 Reorganeze the structure of the document 2017-05-17 09:50:13 +02:00
regnat
7ac9eb8533 Move every subsection into ints own file 2017-05-17 09:36:57 +02:00
regnat
5923287986 Separate compilation and pre-processing 2017-05-17 09:22:11 +02:00
regnat
cd6e2483ff Use a union-like operator for the union of arrows 2017-05-16 18:15:02 +02:00
regnat
6da4677d73 Use a less ugly symbol for the \subtypeG operator 2017-05-16 16:31:01 +02:00
regnat
fecb548bcd Fix annotation typing rule for patterns 2017-05-16 16:30:20 +02:00
regnat
585ecdce64 Add definition of the type accepted by a pattern 2017-05-16 16:26:52 +02:00
regnat
2f81b57378 Replace itemize by description in compilation 
This makes the formatting of the paragraph much nicer
 2017-05-16 13:42:20 +02:00
regnat
c165884a4c Make type checking example syntactically correct 2017-05-16 13:42:20 +02:00
regnat
c459939d64 Typos 2017-05-16 13:42:14 +02:00
regnat
8240f10043 Remove leftover let rec 2017-05-16 12:51:28 +02:00
regnat
252e76c791 typing rules: fix nits 2017-05-16 12:50:07 +02:00
regnat
d7c3f96282 Use projections in the typing of patterns 2017-05-16 09:44:16 +02:00
regnat
bdb31f74b2 Fix display of pattern matchic sematic rules 2017-05-16 09:42:26 +02:00
regnat
1f10bc7da8 Change link to the paper in the readme 2017-05-16 09:29:24 +02:00
regnat
1434c00ca8 Slightly improve the display of reduction rules 2017-05-16 09:24:32 +02:00
regnat
1a593f1436 Remove record types from grammar 2017-05-16 09:11:14 +02:00
regnat
3eea4d3bfc Remove patterns from the typing rules 2017-05-16 09:09:25 +02:00
regnat
ce1d1395d5 Replace pairs by lists in nix-light grammar 2017-05-16 08:00:22 +02:00
regnat
1bbd757531 Simplify the semantics of pattern-matching 2017-05-16 08:00:07 +02:00
regnat
4b8cd5bd3f make the definition of \var global 2017-05-16 07:53:04 +02:00
regnat
6fe5710f8f Update rediction rules for the λ-calculus 2017-05-16 07:49:39 +02:00
regnat
d4e6ed6d6c Write the semantics of the compilation 2017-05-15 17:42:21 +02:00
regnat
a6aa3f804b Add note (in plaintext) about the compilation 2017-05-15 17:07:26 +02:00
regnat
f1450cdc29 Add nix grammar 
Only the λ-calculus subset with lists
 2017-05-15 15:48:06 +02:00
regnat
fa9459a369 Add example for the \A function 2017-05-15 15:21:43 +02:00
regnat
f360efc209 Add a part about top-down type-checking 2017-05-15 14:36:22 +02:00
regnat
824bcdbf2e move lacheck -n11 option to makefile 2017-05-12 19:03:28 +02:00
regnat
368ac2906b Add reference to regnat/tix in the readme 2017-05-12 19:00:10 +02:00
regnat
7e92346903 Explain the \delta in typing rules 2017-05-12 16:59:29 +02:00
regnat
f7e9b52c8c Add a paragraph about the bidirectional typing 2017-05-12 16:40:05 +02:00