# Tag Info

34

Software Foundations by Benjamin C. Pierce would be a good place to start. It would be a make a good precursor to his Types and Programming Languages. There is also Simon Thompson's Type Theory and Functional Programming and Girard's Proofs and Types.

22

I can think of a few possible answers coming from linear logic. The simplest one is the affine lambda-calculus: consider only lambda-terms in which every variable appears at most once. This condition is preserved by reduction and it is immediate to see that the size of affine terms strictly decreases with each reduction step. Therefore, the untyped affine ...

21

A recent developpement on this topic: U. dal Lago and B. Accatoli proved that the length of the leftmost-outermost reduction (LOr) of a $\lambda$-term is an invariant (time) cost model for $\lambda$-calculus. They show that Turing machines (with cost=time) and $\lambda$-terms (with cost=length of the LOr) can simulate each other with a polynomial overhead ...

20

All of the following comments are premised on the choice of a standard implementation strategy using closures to represent function values and a call-by-value evaluation order: For the pure lambda calculus, garbage collection is not necessary. This is because it is not possible to form cycles in the heap: every newly-allocated value can only contain ...

20

Roughly speaking, there are two main strategies for safe manual memory management. The first approach is to use some substructural logic like linear logic to control resource usage. This idea has floated around basically since linear logic's inception, and basically works on the observation that by banning the structural rule of contraction, every variable ...

17

Abstract interpretation is a very general concept and depending on whom you ask, you will receive different explanations because versatile concepts admit multiple perspectives. The view in this answer is mine and I would not assume it is general. Computational hardness as a motivation Let's start with decision problems, whose solutions have a structure ...

17

There have been a number of developments with regards to the use of monads in the theory of computation since Eugenio Moggi's work. I am not able to give a comprehensive account, but here are some points that I am familiar with, others can chime in with their answers. Specific examples of monads You do not have to study super-general theory all the time. ...

15

You might want to check out Liquid Haskell, which allow working with type refinements rather than dependent types. Type refinements can be seen as a restricted logical language that allow you to express Hoare-style properties of the inhabitants of various datatypes. Another possible candidate is the $F^*$ language, which offers similar constructs. There ...

15

One apparent strength of his approach is that it allows higher-order functions (i.e. lambda terms) to be observable outcomes, which measure theory generally makes quite tricky. (The basic problem is that spaces of measurable functions generally have no Borel $\sigma$-algebra for which the application function - sometimes called "eval" - is measurable; see ...

15

I think you are asking about two different things. The ability of a programming language to represent all its programs as data. Reasoning about programs as data. For analytical purposes it's useful to keep them apart. I will focus on the former. The ability of a programming languages to represent, manipulate (and run) its programs as data goes ...

14

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense. Structural operational semantics is not denotational, because it is not a compositional method of giving semantics to a programming language. However, you can build denotational models out of a structural operational semantics by using a ...

14

As I said in my comment, the answer in general is no. The important point to understand (I say this for Viclib, who seems to be learning about these things) is that having a programming language/set of machines in which all programs/computations terminate by no means implies that function equality (i.e., whether two programs/machines compute the same ...

14

Yes, your type inference seems incomplete. This example can be dealt with fairly trivially, by computing the respective type equations, e.g. in the style Hindley/Milner does it. Alpha-renaming the example makes it easier to follow: ((\x.x) (\y.y)) 10 For maximum clarity, let's start by assigning type variables to each sub expression: x : A (\x.x) : B y : C ...

14

In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra $\cal A$, and to represent types as a ($n$-ary) relation $R \subseteq \cal A^n$. This works perfectly fine for all kinds of type theories, including dependently typed theories, see e.g. ...

14

The overall purpose of PLT is to make industrial software engineering (in a general sense) cheaper (also in a general sense), through optimising the most important tool (programming languages) and associated tooling ecosystem. Some reasons why maths is involved: PLs are highly non-trivial, and it's not clear that they do the right thing without proof. ...

13

Comparing two programming languages is difficult is a difficult problem, and far from being solved. The key issue is that there are many different ways languages can be compared, and none of them is compelling. The most widely used approach, coming from logic, is to consider translations between the languages to be compared. The general idea is as ...

13

Honda and Yoshida's A Compositional Program Logic for Polymorphic Higher-Order Functions (probably) pioneered Hoare logics for purely functional languages. This work is based on Hennessy-Milner logic and Milner's encoding of functions into processes, as described here: From Process Logic to Program Logic The work by Régis-Gianas et al mentioned in ...

12

Unfortunately, there are too many things are going on here. So, it is easy to mix things up. The use of "full" in "full completeness" and "full abstraction" refer to completely different ideas of fullness. But, there is also some vague connection between them. So, this is going to be a complicated answer. Full completeness: "Sound and complete" is a ...

12

The original paper by Church and Rosser, "Some Properties of Conversion," describes something that may be an example of what you're looking for. If you use the strict lambda calculus, where in every occurrence of $\lambda x.M$ you have that $x$ appears free in $M$, then without a type system the following property holds (it's Theorem 2 in Church and Rosser'...

12

You are correct when you observe that for any particular terminating loop $L$ we may simply define the invariant "we're getting one step closer to termination". But proving that this is indeed a valid invariant may require transfinite induction! For instance, we could write a loop that computes the Goodstein sequence. This is particular sequence of numbers ...

11

If I am not mistaken the simulations between Turing machines and $\lambda$-calculus can be accomplished with a polynomial-time slowdown. Of course, for this to make sense we need to specify an evaluation strategy and measure of cost for $\lambda$-calculus but I am sure something reasonable can be found. You ask about numbers in particular. Of course Church ...

11

There are absolutely some relationships between the semantics and practice of OOP and category theory. This is somewhat unsurprising since both fields attempt to give a principled generic account of structure and behavior in a synthetic manner. The most apparent work I am aware of is the categorical semantics of UML, which is admittedly different from OOP ...

11

Barendregts Lambda Calculi with Types is more advanced, but it covers some important topics in the "classical" theory of types.

11

See also Yann Régis-Gianas PhD thesis work with François Pottier: A Hoare Logic for Call-by-Value Functional Programs (MPC'08). This work was extended to cover the usual ML side-effects by Johannes Kanig and Jean-Cristophe Filliatre in 2009: Who: A Verifier for Effectful Higher-order Programs.

11

I know of: Jan M. Smith, The independence of Peano's fourth axiom from Martin-Löf's type theory without universes, The Journal of Symbolic Logic 53(3), p. 840-845, 1988.

11

Blum’s speedup theorem is usually stated in the language of partially recursive functions, but up to trivial differences in notation, it works just the same in the language of $\lambda$-calculus. It says that given any reasonable complexity measure $M$ (for example, the optimal number of reductions as in the question) and a recursive function $f(x,y)$ (for ...

11

Yes, it's impossible to have a nondegenerate CCC with general recursion and categorical coproducts. The standard reference for this is: H. Huwig and A. Poigne. A note on inconsistencies caused by fixpoints in a cartesian closed category. Theoretical Computer Science, 73:101–112, 1990. However, I and (most of the other people I've met) learned about it ...

11

From a programming language theory perspective, as opposed to the computability perspective other answers and comments have offered, C++ templates combined with concepts correspond to bounded polymorphism or constrained genericity. Concepts themselves correspond to the constraints or bounds placed on a type. A template is type-level function, parameterised ...

11

No, to my knowledge there has been no work on formalizing TeX of the kind you are interested in. (What follows is a subjective and personal commentary). I think it is an intriguing and well-posed idea, and your motivation of using it to perform optimizations sounds reasonable -- another related question is whether you could define a bytecode format for it ...

11

Andrej's and Łukasz's answers make good points, but I wanted to add additional comments. To echo what Damiano said, this way of representing binding using pointers is the one suggested by proof-nets, but the earliest place where I saw it for lambda terms was in an old essay by Knuth: Donald Knuth (1970). Examples of formal semantics. In Symposium on ...

Only top voted, non community-wiki answers of a minimum length are eligible