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
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
