The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus (Q4972064): Difference between revisions

Latest revision as of 09:03, 31 July 2024

scientific article; zbMATH DE number 7135413

Language	Label	Description	Also known as
English	The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus	scientific article; zbMATH DE number 7135413

Statements

instance of

scholarly article

0 references

title

The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus (English)

0 references

0 references

0 references

Journal of Functional Programming

0 references

publication date

22 November 2019

0 references

describes a project that uses

ML

0 references

PoplMark

0 references

MaRDI profile type

MaRDI publication profile

0 references

cites work

Explicit substitutions

0 references

The Useful MAM, a Reasonable Implementation of the Strong $$\lambda $$ -Calculus

0 references

Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus

0 references

A Strong Distillery

0 references

Engineering formal metatheory

0 references

Theorem Proving in Higher Order Logics

0 references

The lambda calculus. Its syntax and semantics. Rev. ed.

0 references

Q4385533

0 references

Needed reduction and spine strategies for the lambda calculus

0 references

A concrete framework for environment machines

0 references

The locally nameless representation

0 references

Strongly reducing variants of the Krivine abstract machine

0 references

Q3785893

0 references

An abstract framework for environment machines

0 references

The duality of computation

0 references

Confluence properties of weak and strong calculi of explicit substitutions

0 references

Combinatory logic. With two sections by William Craig.

0 references

From Reduction-Based to Reduction-Free Normalization

0 references

Q5667469

0 references

Q4510397

0 references

A compiled implementation of strong reduction

0 references

Q3774923

0 references

Formal verification of parallel programs

0 references

The Theory of Calculi with Explicit Substitutions Revisited

0 references

A Theory of Explicit Substitutions with Safe and Full Composition

0 references

$\lambda$ to SKI, semantically -- declarative pearl

0 references

A call-by-name lambda-calculus machine

0 references

Explicit substitutions with de bruijn's levels

0 references

0 references

0 references

0 references

0 references

Call-by-name, call-by-value and the $\lambda$-calculus

0 references

Parametric parameter passing $\lambda$-calculus

0 references

Full Reduction in the Face of Absurdity

0 references

Q4414741

0 references

full work available at URL

https://doi.org/10.1017/s0956796819000017

0 references

Identifiers

zbMATH Open document ID

1493.68085

0 references

DOI

10.1017/S0956796819000017

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

0 references

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:4972064

@@ Property / describes a project that uses @@
+PoplMark
@@ Property / describes a project that uses: PoplMark / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Explicit substitutions
@@ Property / cites work: Explicit substitutions / rank @@
+Normal rank
@@ Property / cites work @@
+The Useful MAM, a Reasonable Implementation of the Strong $$\lambda $$ -Calculus
+Normal rank
@@ Property / cites work @@
+Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
+Normal rank
@@ Property / cites work @@
+A Strong Distillery
@@ Property / cites work: A Strong Distillery / rank @@
+Normal rank
@@ Property / cites work @@
+Engineering formal metatheory
@@ Property / cites work: Engineering formal metatheory / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+Normal rank
@@ Property / cites work @@
+Q4385533
@@ Property / cites work: Q4385533 / rank @@
+Normal rank
@@ Property / cites work @@
+Needed reduction and spine strategies for the lambda calculus
+Normal rank
@@ Property / cites work @@
+A concrete framework for environment machines
@@ Property / cites work: A concrete framework for environment machines / rank @@
+Normal rank
@@ Property / cites work @@
+The locally nameless representation
@@ Property / cites work: The locally nameless representation / rank @@
+Normal rank
@@ Property / cites work @@
+Strongly reducing variants of the Krivine abstract machine
+Normal rank
@@ Property / cites work @@
+Q3785893
@@ Property / cites work: Q3785893 / rank @@
+Normal rank
@@ Property / cites work @@
+An abstract framework for environment machines
@@ Property / cites work: An abstract framework for environment machines / rank @@
+Normal rank
@@ Property / cites work @@
+The duality of computation
@@ Property / cites work: The duality of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Confluence properties of weak and strong calculi of explicit substitutions
+Normal rank
@@ Property / cites work @@
+Combinatory logic. With two sections by William Craig.
+Normal rank
@@ Property / cites work @@
+From Reduction-Based to Reduction-Free Normalization
+Normal rank
@@ Property / cites work @@
+Q5667469
@@ Property / cites work: Q5667469 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4510397
@@ Property / cites work: Q4510397 / rank @@
+Normal rank
@@ Property / cites work @@
+A compiled implementation of strong reduction
@@ Property / cites work: A compiled implementation of strong reduction / rank @@
+Normal rank
@@ Property / cites work @@
+Q3774923
@@ Property / cites work: Q3774923 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal verification of parallel programs
@@ Property / cites work: Formal verification of parallel programs / rank @@
+Normal rank
@@ Property / cites work @@
+The Theory of Calculi with Explicit Substitutions Revisited
+Normal rank
@@ Property / cites work @@
+A Theory of Explicit Substitutions with Safe and Full Composition
+Normal rank
@@ Property / cites work @@
+\(\lambda\) to SKI, semantically -- declarative pearl
+Normal rank
@@ Property / cites work @@
+A call-by-name lambda-calculus machine
@@ Property / cites work: A call-by-name lambda-calculus machine / rank @@
+Normal rank
@@ Property / cites work @@
+Explicit substitutions with de bruijn's levels
@@ Property / cites work: Explicit substitutions with de bruijn's levels / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024846
@@ Property / cites work: Q3024846 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5687569
@@ Property / cites work: Q5687569 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4692880
@@ Property / cites work: Q4692880 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2778806
@@ Property / cites work: Q2778806 / rank @@
+Normal rank
@@ Property / cites work @@
+Call-by-name, call-by-value and the \(\lambda\)-calculus
+Normal rank
@@ Property / cites work @@
+Parametric parameter passing \(\lambda\)-calculus
@@ Property / cites work: Parametric parameter passing \(\lambda\)-calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Full Reduction in the Face of Absurdity
@@ Property / cites work: Full Reduction in the Face of Absurdity / rank @@
+Normal rank
@@ Property / cites work @@
+Q4414741
@@ Property / cites work: Q4414741 / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0956796819000017
+Normal rank
@@ Property / OpenAlex ID @@
+W2943029224
@@ Property / OpenAlex ID: W2943029224 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q127959945
@@ Property / Wikidata QID: Q127959945 / rank @@
+Normal rank