40

A type $C$ has a logarithm to base $X$ of $P$ exactly when $C \cong P\to X$. That is, $C$ can be seen as a container of $X$ elements in positions given by $P$. Indeed, it's a matter of asking to what power $P$ we must raise $X$ to obtain $C$. It makes sense to work with $\mathop{log}F$ where $F$ is a functor, whenever the logarithm exists, meaning $\mathop{...


30

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.


25

As it happens, I'm writing a paper about this now. IMO, a good way to think about futures or promises is in terms of the Curry-Howard correspondence for temporal logic. Basically, the idea behind futures is that it is a data structure representing a computation that is in progress, and upon which you can synchronize. In terms of temporal logic, this is the ...


24

I think the overall goal of PL theory is to lower the cost of large-scale programming by way of improving programming languages and the techincal ecosystem wherein languages are used. Here are some high-level, somewhat vague descriptions of PL research areas that have received sustained attention, and will probably continue to do so for a while. Most ...


23

Yes, it is. Here's how you do it: You can compile basically any program you like to circuits. See for instance the work of Dan Ghica and his collaborators on the Geometry of Synthesis, which shows how to compile programs into circuits. Dan R. Ghica. Geometry of Synthesis: A structured approach to VLSI design Dan R. Ghica, Alex Smith. Geometry of Synthesis ...


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

The short answer is no. The long answer is that such languages are invented on a regular basis, but if they see any significant degree of use, for good semantic reasons they never remain in this mode for very long. The basic problem is that it is very difficult to build programs compositionally using state machines. The modular construction of programs ...


20

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

What you want exists, and is an enormous area of research: it's the entire theory of programming languages. Loosely speaking, you can view computation in two ways. You can think of machines, or you can think of languages. A machine is basically some kind of finite control augmented with some (possibly unbounded) memory. This is why introductory TOC ...


19

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


18

"Meaning" is used in a broader way than denotation is. The original dichotomy, inherited from logic and philosophy, is between "sense" and "denotation" (which philosophers call "reference"). This distinction can be illustrated by Frege's original example. He noted that phrases "the morning star" and "the evening star" referred to the same object --- the ...


18

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


16

It depends on the total functional language. This answer sounds like a cop-out, but nothing more specific can be said. After all, consider whatever important decidable program that you're interested in. Write a program in your favorite Turing-complete language to solve it. Since the problem is decidable, your program will halt on all inputs. (Arguably, a ...


16

What are the limitations of total functional programming? It is not Turing-complete, but still supports a large subset of the possible programs. Are there important constructs that you could write in a Turing-complete language, but not in a total functional language? Assuming your functional language $L$ lets you encode arithmetic operations, there is one ...


16

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


16

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

Proof nets are interesting essentially for three reasons: 1) IDENTITY OF PROOFS. They provide an answer to the problem "when are two proofs the same"? In sequent calculus you may have many different proofs of the same proposition which differ only because sequent calculus forces an order among deduction rules even when this is not necessary. Of course, one ...


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


14

Let us call a logic "symmetric" where a $-A$ ("not A") assumption means the same as proving $A$ and a proof of $-A$ means the same as an assumption of $A$. Classical logic and linear logic are symmetric in this sense. Intuitionistic logic is not. Girard noticed that natural deduction is asymmetric in exactly this way. That is why it matches up with ...


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

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

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

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

You probably want Manna, Pnueli, Axiomatic Approach to Total Correctness of Programs, 1973


13

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


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

Let me list some assumptions which limit the programming language research. These are hard to break away from because they feel like they are an essential part of what programming languages are about, or because exploring alternatives would be "not programming language design anymore". With each assumption I list its limiting effects. Programs are syntactic ...


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