Recursive functions of symbolic expressions and their computation by machine, Part I
From MaRDI portal
Publication:3283220
DOI10.1145/367177.367199zbMath0101.10413OpenAlexW2045255985WikidataQ54157473 ScholiaQ54157473MaRDI QIDQ3283220
Publication date: 1960
Published in: Communications of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/367177.367199
Related Items (71)
Unified selection from lists, arrays, and objects. ⋮ Verifying Procedural Programs via Constrained Rewriting Induction ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ JEFL: joint embedding of formal proof libraries ⋮ Unnamed Item ⋮ GC\(^{2}\): a generational conservative garbage collector for the ATERM library ⋮ Deep Generation of Coq Lemma Names Using Elaborated Terms ⋮ Java for high-performance network-based computing: a survey ⋮ A combinatory account of internal structure ⋮ Classes of equational programs that compile into efficient machine code ⋮ A \(\pi\)-calculus with explicit substitutions ⋮ Functional programming with combinators ⋮ Directly reflective meta-programming ⋮ Parallel scheduling of recursively defined arrays ⋮ Proving termination of context-sensitive rewriting by transformation ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Linear logic automata ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A syntactic correspondence between context-sensitive calculi and abstract machines ⋮ Programs=data=first-class citizens in a computational world ⋮ Equivalence checking of two functional programs using inductive theorem provers ⋮ Deaccumulation techniques for improving provability ⋮ A π-calculus with explicit substitutions: The late semantics ⋮ To every manifest domain a CSP expression -- a rôle for mereology in computer science ⋮ Analytical study of cubature formulas on a sphere in computer algebra systems ⋮ Efficient, verified checking of propositional proofs ⋮ Using dynamic memory reallocation in GInv ⋮ Term rewriting for normalization by evaluation. ⋮ John McCarthy (1927--2011) ⋮ An efficient approach to cyclic reference counting based on a coarse-grained search ⋮ When Logic Meets Engineering: Introduction to Logical Issues in the History and Philosophy of Computer Science ⋮ Reversible computing from a programming language perspective ⋮ Structural operational semantics through context-dependent behaviour ⋮ Recursive data structures ⋮ Modeling of storage properties of higher-level languages ⋮ Unnamed Item ⋮ A survey of state vectors ⋮ Metacircularity in the polymorphic \(\lambda\)-calculus ⋮ Agent-Based Modeling and Computer Languages ⋮ Logic and functional programming by retractions ⋮ Distributed quantum programming ⋮ External and internal syntax of the \(\lambda \)-calculus ⋮ Computer theorem proving in mathematics ⋮ A glimpse into the paradise of combinatory algebra ⋮ Functional parallel typified language and its implementation on clusters ⋮ A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs ⋮ Algebraic correctness proofs for compiling recursive function definitions with strictness information ⋮ Context-sensitive dependency pairs ⋮ Automatic program indentation ⋮ Testing equality in lisp-like environments ⋮ Recursive converters on a memory ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ Limited second-order functionality in a first-order setting ⋮ A Verified Runtime for a Verified Theorem Prover ⋮ A Groupoid of Isomorphic Data Transformations ⋮ N-ary selection functions and formal selective systems. I ⋮ The lambda-gamma calculus: A language adequate for defining recursive functions ⋮ From Reduction-Based to Reduction-Free Normalization ⋮ A portable lisp compiler ⋮ Implementing Compositional Analysis Using Intersection Types With Expansion Variables ⋮ Experience with software conversion ⋮ A data structure formalization through generating function ⋮ Theory of symbolic expressions. I ⋮ Encoding many-valued logic in $\lambda$-calculus ⋮ Context-sensitive rewriting strategies ⋮ Closure functions and general iterates as reflectors ⋮ A category theory for programming languages ⋮ Logical debugging ⋮ A framework for modeling the semantics of synchronous and asynchronous procedures with abstract state machines
Uses Software
This page was built for publication: Recursive functions of symbolic expressions and their computation by machine, Part I
