Automatic synthesis of typed $\Lambda$-programs on term algebras

DOI10.1016/0304-3975(85)90135-5zbMath0597.68017OpenAlexW1513579486MaRDI QIDQ1079357

Publication date: 1985

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(85)90135-5

zbMATH Keywords

data structures completeness theorem equivalence of programs primitive recursive functions automatic synthesis of programs data system finitary term algebra Iterative functions second- order typed lambda-calculus

Mathematics Subject Classification ID

Recursive functions and relations, subrecursive hierarchies (03D20) Free algebras (08B20) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items

Inductively defined types in the Calculus of Constructions, Algebraic types in PER models, Types as parameters, The Girard-Reynolds isomorphism, Equational programming in $\lambda$-calculus via SL-systems. Part 1, Algorithmically broad languages for polynomial time and space, An application of PER models to program extraction, Categorical data types in parametric polymorphism, Constructive natural deduction and its ‘ω-set’ interpretation, On Church's formal theory of functions and functionals. The $\lambda$- calculus: Connections to higher type recursion theory, proof theory, category theory, Defining data structures via Böhm-out, Push versus pull-based loop fusion in query engines, The Girard-Reynolds isomorphism (second edition), Parametricity of extensionally collapsed term models of polymorphism and their categorical properties, Intersection and union types, An extension of system F with subtyping, Programming with streams in Coq a case study: The Sieve of Eratosthenes, Classical (co)recursion: Mechanics, Many more predecessors: A representation workout, Types, abstraction, and parametric polymorphism, part 2, Efficiency of lambda-encodings in total type theory, The calculus of dependent lambda eliminations, Unnamed Item, Bifibrational functorial semantics of parametric polymorphism, Lambda calculus with patterns, Polynat in PER models, The Impact of the Lambda Calculus in Logic and Computer Science, Metacircularity in the polymorphic $\lambda$-calculus, Recursive programming with proofs, Comparing Hagino's categorical programming language and typed lambda- calculi, Incorporating quotation and evaluation into Church's type theory, On list primitive recursion and the complexity of computing inf, A CuCh Interpretation of an Object-Oriented Language1 1Partially supported by MURST Cofin '99 TOSCA., Program morphisms, Preface to the special volume, Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism, Introduction to Type Theory, Least and greatest fixed points in intuitionistic natural deduction, Constant time parallel computations in $\lambda$-calculus, On the proof theory of Coquand's calculus of constructions, Strong storage operators and data types, Extensional models for polymorphism, Functorial polymorphism, Structures definable in polymorphism, Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages, Complete Types in an Extension of the System AF2, Two extensions of system F with (co)iteration and primitive (co)recursion principles, Proofs for free, Ramified recurrence and computational complexity. III: Higher type recurrence and elementary complexity, LAMBDA-REPRESENTABLE FUNCTIONS OVER TERM ALGEBRAS, Type Theories from Barendregt’s Cube for Theorem Provers, Ordinals and ordinal functions representable in the simply typed lambda calculus, Encoding many-valued logic in $\lambda$-calculus, $\lambda$-definability of free algebras, Formal parametric polymorphism, Functions over free algebras definable in the simply typed lambda calculus, Combining type disciplines

Cites Work

Automatic synthesis of typed \(\Lambda\)-programs on term algebras