[\lambda\delta home]
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
[Spacer]

home news specification

documentation implementation
foreword milestones version 2 (background - syntax - core - applications)
version 2 helena Open Symbolic Notation (OSN)
citations visibility version 1 (background - core) (static HELM directory) version 1 library (static LDDL directory)
Contents of the Specification [butterfly]
This specification comprises a collection of checked applications of λδ version 2. In particular it contains the components below.
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline.
category units




sizes characters (files) 17225 (26) nodes (objects) 53039 (85) intrinsic loss factor 3.1
propositions theorems 5 lemmas 48 total 53
concepts declared 5 defined 19 total 24
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
component plane files

models term model tm ( ⇡[?]? ) ( ⇡[?←?]? ) tm_exteq

denotational equivalence deq ( ? ⊢ ? ≗{?} ? ) deq_cpr

local environment interpretation li ( ? ϵ ⟦?⟧{?}[?] ) li_vpushs

multiple evaluation push vpushs ( ?⨁{?}[?]? ≘ ? ) vpush_fold

evaluation equivalence veq ( ? ≗{?} ? ) veq_lifts

model declaration model ( ? ≗{?} ? ) ( ? @{?} ? ) ( ⟦?⟧{?}[?,?] ) model_vpush ( ⫯{?}[?←?]? ) model_props
functional relocation flifts ( ↑*[?]? ) ( ↑[?]? ) flifts_basic ( ↑[?,?]? )
examples terms with special features ex_cpr_omega

[Spacer]

[Valid XHTML 1.1] [Valid CSS level 2] [Generated from XML via XSL] [PNG used here] [Viewable with any browser]

Last update: Fri, 13 Jul 2018 17:34:24 +0200