Call-by-value lambda calculus as a model of computation in Coq (Q2319993): Difference between revisions

@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-018-9484-2
+Normal rank
@@ Property / OpenAlex ID @@
+W3022819504
@@ Property / OpenAlex ID: W3022819504 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5111892
@@ Property / cites work: Q5111892 / rank @@
+Normal rank
@@ Property / cites work @@
+(Leftmost-Outermost) Beta Reduction is Invariant, Indeed
+Normal rank
@@ Property / cites work @@
+Formalizing Turing Machines
@@ Property / cites work: Formalizing Turing Machines / rank @@
+Normal rank
@@ Property / cites work @@
+A formalization of multi-tape Turing machines
@@ Property / cites work: A formalization of multi-tape Turing machines / rank @@
+Normal rank
@@ Property / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+Normal rank
@@ Property / cites work @@
+Q2852343
@@ Property / cites work: Q2852343 / rank @@
+Normal rank
@@ Property / cites work @@
+Computability and Logic
@@ Property / cites work: Computability and Logic / rank @@
+Normal rank
@@ Property / cites work @@
+The Independence of Markov's Principle in Type Theory.
+Normal rank
@@ Property / cites work @@
+The weak lambda calculus as a reasonable machine
@@ Property / cites work: The weak lambda calculus as a reasonable machine / rank @@
+Normal rank
@@ Property / cites work @@
+Weak call-by-value lambda calculus as a model of computation in Coq
+Normal rank
@@ Property / cites work @@
+TWO RECURSIVELY ENUMERABLE SETS OF INCOMPARABLE DEGREES OF UNSOLVABILITY (SOLUTION OF POST'S PROBLEM, 1944)
+Normal rank
@@ Property / cites work @@
+Q4506483
@@ Property / cites work: Q4506483 / rank @@
+Normal rank
@@ Property / cites work @@
+Programming in the λ-Calculus: From Church to Scott and Back
+Normal rank
@@ Property / cites work @@
+Q4344149
@@ Property / cites work: Q4344149 / rank @@
+Normal rank
@@ Property / cites work @@
+Typing total recursive functions in Coq
@@ Property / cites work: Typing total recursive functions in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient self-interpretation in lambda calculus
@@ Property / cites work: Efficient self-interpretation in lambda calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Q3232283
@@ Property / cites work: Q3232283 / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanised Computability Theory
@@ Property / cites work: Mechanised Computability Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Call-by-name, call-by-value and the \(\lambda\)-calculus
+Normal rank
@@ Property / cites work @@
+Recursively enumerable sets of positive integers and their decision problems
+Normal rank
@@ Property / cites work @@
+A variant of a recursively unsolvable problem
@@ Property / cites work: A variant of a recursively unsolvable problem / rank @@
+Normal rank
@@ Property / cites work @@
+A Declarative Language for the Coq Proof Assistant
+Normal rank
@@ Property / cites work @@
+Q4385524
@@ Property / cites work: Q4385524 / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanising Turing Machines and Computability Theory in Isabelle/HOL
+Normal rank