The lambda calculus and its relation to programming languages

1972 ◽  
Author(s):  
Arthur Evans
Keyword(s):  
Programming Languages ◽  
Lambda Calculus

Decoupling IPv7 from Replication in Link-Level Acknowledgements

2012 ◽  
Vol 246-247 ◽  
pp. 390-393
Author(s):  
Yu Hui Shen ◽  
Han Zhou Hao
Keyword(s):  
Model Checking ◽  
Programming Languages ◽  
Lambda Calculus ◽  
Position Paper ◽  
The Internet ◽  
Game Theoretic

Mathematicians agree that homogeneous archetypes are an interesting new topic in the field of programming languages, and researchers concur. In our research, we verify the evaluation of model checking. In this position paper we describe an encrypted tool for refining lambda calculus (VENDS), which we use to prove that the Internet can be made empathic, game-theoretic, and metamorphic.

Linearization of the lambda-calculus and its relation with intersection type systems

2004 ◽  
Vol 14 (5) ◽  
pp. 519-546 ◽  
Author(s):  
MÁRIO FLORIDO ◽  
LUÍS DAMAS
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Type System ◽  
Lambda Calculus ◽  
Type Systems ◽  
Functional Programming Languages

In this paper we present a notion of expansion of a term in the lambda-calculus which transforms terms into linear terms. This transformation replaces each occurrence of a variable in the original term by a fresh variable taking into account non-trivial implications in the structure of the term caused by these simple replacements. We prove that the class of terms which can be expanded is the same of terms typable in an Intersection Type System, i.e. the strongly normalizable terms. We then show that expansion is preserved by weak-head reduction, the reduction considered by functional programming languages.

scholarly journals Compiler Generation from Denotational Semantics

1980 ◽  
Vol 9 (113) ◽  
Author(s):  
Neil D. Jones
Keyword(s):  
Programming Languages ◽  
State Transition ◽  
Lambda Calculus ◽  
Denotational Semantics ◽  
Optimization Methods ◽  
Compiler Generation ◽  
Syntax Rule ◽  
Language L ◽  
Algebraic Framework ◽  
Efficient Code

<p>A methodology is described for generating provably correct compilers from denotational definitions of programming languages. An application is given to produce compilers into STM code (an STM or state transition machine is a flow-chart-like program, low-level enough to be translated into efficient code on conventional computers). First, a compiler phi: LAMC -&gt; STM from a lambda calculus dialect is defined. Any denotational definition DD of language L defines a map DD': L -&gt; LAMC, so DD'_circle phi compiles L into STM code. Correctness follows from the correctness of phi.</p><p>The algebraic framework of Morris, ADJ, etc. is used. The set of STMs is given an algebraic structure so any DD'_circ phi may be specified by giving a derived operator on STM for each syntax rule of L.</p><p>This approach yields quite redundant object programs, so the paper ends by describing two flow analytic optimization methods. The first analyzes an already-produced STM to obtain information about its runtime behaviour which is used to optimize the STM. The second analyzes the generated compiling scheme to determine runtime properties of object programs in general which a compiler can use to produce less redundant STMs.</p>

scholarly journals Label dependent lambda calculus and gradual typing

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-29
Author(s):  
Weili Fu ◽  
Fabian Krause ◽  
Peter Thiemann
Keyword(s):  
Programming Languages ◽  
Lambda Calculus ◽  
Dependent Types ◽  
Type Checking ◽  
Original Language ◽  
Type Reduction ◽  
Wide Range ◽  
Gradual Typing ◽  
Class Labels

Dependently-typed programming languages are gaining importance, because they can guarantee a wide range of properties at compile time. Their use in practice is often hampered because programmers have to provide very precise types. Gradual typing is a means to vary the level of typing precision between program fragments and to transition smoothly towards more precisely typed programs. The combination of gradual typing and dependent types seems promising to promote the widespread use of dependent types. We investigate a gradual version of a minimalist value-dependent lambda calculus. Compile-time calculations and thus dependencies are restricted to labels, drawn from a generic enumeration type. The calculus supports the usual Pi and Sigma types as well as singleton types and subtyping. It is sufficiently powerful to provide flexible encodings of variant and record types with first-class labels. We provide type checking algorithms for the underlying label-dependent lambda calculus and its gradual extension. The gradual type checker drives the translation into a cast calculus, which extends the original language. The cast calculus comes with several innovations: refined typing for casts in the presence of singletons, type reduction in casts, and fully dependent Sigma types. Besides standard metatheoretical results, we establish the gradual guarantee for the gradual language.

Theoretical Pearls: Self-interpretation in lambda calculus

1991 ◽  
Vol 1 (2) ◽  
pp. 229-233 ◽  
Author(s):  
Henk Barendregt
Keyword(s):  
Normal Form ◽  
Programming Languages ◽  
Lambda Calculus ◽  
Direct Consequence ◽  
Functional Program ◽  
Computer Scientists ◽  
Strange Loop ◽  
Reduction Machine ◽  
Image Position ◽  
Computable Functions

Programming languages which are capable of interpreting themselves have been fascinating computer scientists. Indeed, if this is possible then a ‘strange loop’ (in the sense of Hofstadter, 1979) is involved. Nevertheless, the phenomenon is a direct consequence of the existence of universal languages. Indeed, if all computable functions can be captured by a language, then so can the particular job of interpreting the code of a program of that language. Self-interpretation will be shown here to be possible in lambda calculus.The set of λ-terms, notation Λ, is defined by the following abstract syntaxwhereis the set {v, v′, v″, v′″,…} of variables. Arbitrary variables are usually denoted by x, y,z,… and λ-terms by M,N,L,…. A redex is a λ-term of the formthat is, the result of substituting N for (the free occurrences of) x in M. Stylistically, it can be said that λ-terms represent functional programs including their input. A reduction machine executes such terms by trying to reduce them to normal form; that is, redexes are continuously replaced by their contracta until hopefully no more redexes are present. If such a normal form can be reached, then this is the output of the functional program; otherwise, the program diverges.

scholarly journals Denotational semantics of recursive types in synthetic guarded domain theory

2018 ◽  
Vol 29 (3) ◽  
pp. 465-510 ◽  
Author(s):  
RASMUS E. MØGELBERG ◽  
MARCO PAVIOTTI
Keyword(s):  
Programming Languages ◽  
Type Theory ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Denotational Semantics ◽  
Domain Theory ◽  
Logical Relation ◽  
Dependent Type Theory ◽  
Semantics Of Programming Languages ◽  
Dependent Type

Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.Working inGuarded Dependent Type Theory(GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types ofGDTT. We prove soundness and computational adequacy of the model inGDTTusing a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.

Redexes are stable in the λ-calculus

2015 ◽  
Vol 27 (5) ◽  
pp. 738-750 ◽  
Author(s):  
JEAN-JACQUES LÉVY
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Stability Property ◽  
Lambda Calculus ◽  
Unique Minimum ◽  
Sequential Programming ◽  
The Stability

In the theory of sequential programming languages, Berry's stability property is an important step claiming that values have unique origins in their calculations. It has been shown that Bohm trees are stable in the λ-calculus, meaning that there is a unique minimum prefix of any lambda term which computes its Bohm tree. Moreover this property is also true for finite prefixes of Bohm trees. The proof relies on Curry's standardization theorem as initially pointed out by Plotkin in his famous articleLCF considered as a programming language. In this paper we will show that the stability property also holds for redexes. Namely for any redex family, there is a unique minimum calculation and a unique redex which computes this family. This property was already known in the study of optimal reductions, but we stress here on stability and want to show that stability is inside the basic objects of calculations. The proof will be based on nice commutations between residuals and creations of new redexes. Our tool for proving this property will be the labelled lambda calculus used in the study of optimal reductions.

Sign in / Sign up

Export Citation Format

Share Document