\lambda\delta home page

$[\lambda\delta home]$

cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)

$\lambda\delta rainbow rule$

Contents of the Specification $\lambda\delta butterfly$

This specification comprises a collection of checked applications of λδ version 2. In particular it contains the components below.

MLTT1. Martin-Löf's Type Theory with one universe using λδ as theory of expressions.

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical account of the specification's contents and its timeline.

2011 December 20. The Functional component is started inside the specification of λδ-2A.

Logical Structure of the Specification $\lambda\delta butterfly$

This table reports the specification's components and their planes.

component	plane	files
models	term model	tm	tm_vpush
	denotational equivalence	deq ( ? ⊢ ? ≗{?} ? )	deq_cpr
	local environment interpretation	li ( ? ϵ ⟦?⟧{?}[?] )	li_vpushs
	multiple evaluation push	vpushs ( ?⨁{?}[?]? ≘ ? )	vpushs_fold
	evaluation equivalence	veq ( ? ≗{?} ? )	veq_lifts
	model declaration	model ( ? ≗{?} ? ) ( ? @{?} ? ) ( ⟦?⟧{?}[?,?] )	model_vpush ( ⫯{?}[?←?]? )	model_props
functional	multiple filling	mf ( ●[?,?]? )	mf_exeq	mf_lifts	mf_cpr
		mf_vpush ( ⇡[?←?]? )	mf_vpush_exteq	mf_vpush_vlift
		mf_vlift ( ⇡[?]? )	mf_vlift_exteq
		mf_v
	relocation	flifts_basic ( ↑[?,?]? )	flifts_flifts_basic
		flifts ( ↑*[?]? ) ( ↑[?]? )	flifts_flifts
examples	terms with special features	ex_cpr_omega ex_rpx_fwd ex_fpbg_refl ex_cnv_eta

$\lambda\delta rainbow rule$

Last update: Tue, 22 Dec 2020 18:19:03 +0100

home	news	specification	specification log		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)