The following pages link to (Q4274979):
Displaying 50 items.
- Graph easy sets of mute lambda terms (Q288793) (← links)
- A relational semantics for parallelism and non-determinism in a functional setting (Q408545) (← links)
- Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus (Q428894) (← links)
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus (Q530864) (← links)
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) (Q636376) (← links)
- Forcing in stable models of untyped \(\lambda\)-calculus (Q698623) (← links)
- Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions (Q764331) (← links)
- Perpetual reductions in \(\lambda\)-calculus (Q1286373) (← links)
- A general storage theorem for integers in call-by-name \(\lambda\)- calculus (Q1329740) (← links)
- Strong normalization for non-structural subtyping via saturated sets (Q1351999) (← links)
- Strong normalization from weak normalization in typed \(\lambda\)-calculi (Q1357009) (← links)
- A semantical storage operator theorem for all types (Q1382182) (← links)
- Computational isomorphisms in classical logic (Q1398471) (← links)
- System ST toward a type system for extraction and proofs of programs (Q1400600) (← links)
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← links)
- A binary modal logic for the intersection types of lambda-calculus. (Q1427854) (← links)
- Behavioural inverse limit \(\lambda\)-models (Q1434350) (← links)
- From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models (Q1583485) (← links)
- Typing total recursive functions in Coq (Q1687755) (← links)
- Strong normalization through intersection types and memory (Q1744407) (← links)
- Non-strictly positive fixed points for classical natural deduction (Q1772778) (← links)
- Building continuous webbed models for system F (Q1826624) (← links)
- Higher order unification via explicit substitutions (Q1854337) (← links)
- Descendants and origins in term rewriting. (Q1854348) (← links)
- Getting results from programs extracted from classical proofs (Q1882897) (← links)
- Simple proof of the completeness theorem for second-order classical and intuitionistic logic by reduction to first-order mono-sorted logic (Q1884882) (← links)
- Intersection types for explicit substitutions (Q1887145) (← links)
- Non-idempotent intersection types in logical form (Q2200821) (← links)
- (In)efficiency and reasonable cost models (Q2333310) (← links)
- Term-generic logic (Q2339466) (← links)
- Fresh logic: Proof-theory and semantics for FM and nominal techniques (Q2372191) (← links)
- The graphical Krivine machine (Q2464713) (← links)
- A call-by-name lambda-calculus machine (Q2464723) (← links)
- Strong Normalizability as a Finiteness Structure via the Taylor Expansion of $$\lambda $$ λ -terms (Q2811355) (← links)
- Reasoning About Call-by-need by Means of Types (Q2811356) (← links)
- Dedekind completion as a method for constructing new Scott domains (Q2841264) (← links)
- Controlling Program Extraction in Light Logics (Q3007661) (← links)
- A Filter Model for the λμ-Calculus (Q3007668) (← links)
- Specifying Imperative ML-Like Programs Using Dynamic Logic (Q3067541) (← links)
- A Relational Model of a Parallel and Non-deterministic λ-Calculus (Q3605523) (← links)
- On the Values of Reducibility Candidates (Q3637200) (← links)
- Focalisation and Classical Realisability (Q3644763) (← links)
- A resource aware semantics for a focused intuitionistic calculus (Q4559602) (← links)
- (Q4580327) (← links)
- Validating Brouwer's continuity principle for numbers using named exceptions (Q4640313) (← links)
- Decidability of all minimal models (Q4647581) (← links)
- On automating the extraction of programs from proofs using product types (Q4916212) (← links)
- (Q4991956) (← links)
- (Q5076060) (← links)
- A Fresh Look at the λ-Calculus (Q5089000) (← links)
