Martin Berger
  • Member for 11 years, 5 months
  • Last seen this week
What should a proof of correctness for a typechecker actually be proving?
Accepted answer
10 votes

The question can be interpreted in two ways: Whether the implementation does implement a given typing system $T$? Whether the typing system $T$ does prevent the errors you think it should? The ...

View answer
Is scope extrusion necessary in the Pi-calculus?
10 votes

Scope extrusion is the key advance of $\pi$-calculus over earlier calculi such as CCS. Scope extrusion is the source of $\pi$-calculus' power of expressing (in a succint and compositional way) other ...

View answer
Ramification of An Impredicative Type Theory
10 votes

One dimension is type inference. System F's type inference for example is not decidable, but some its predicative fragments have decidable (partial) type inference. Another dimension is consistency ...

View answer
Homoiconic languages which are not Turing complete
Accepted answer
9 votes

You can turn every programming language $L$ into a homoiconic language $L_{hom}$ by adding a suitable representation of programs, such as ASTs (abstract syntax trees) or quasi-quoted programs, ...

View answer
Theoretical computer science self-study resources for programmers
9 votes

There are several ways to learn about type theory. For a working programmer, Types and Programming Languages by B. Pierce is a good start. Practical Foundations for Programming Languages by R. ...

View answer
What is the significance of nominal techniques?
9 votes

Short answer. Formal reasoning about binding and $\alpha$-conversion with nominal approaches is closer to intuitive reasoning than alternative approaches. Longer answer. Binders arise everywhere in ...

View answer
Is there a theory of computation that takes failure and decay of the computation substrate into account?
Accepted answer
9 votes

I'm not 100% sure what the question is about, but the title seems to ask about computation that allows failure. There is a lot of work on noisy (erroneous) computation in the sense that I think you ...

View answer
What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?
Accepted answer
9 votes

The definition is straightforward and can be found e.g. in (1, 2), see also (3). Here is a short summary, using a typed $\lambda$-calculus as basis. Types are not really needed for the presentation of ...

View answer
Use of Process Calculi and PL Theory for modern programming language development
9 votes

My answer is really just an elaboration of Gilles', that I had not read before I wrote mine. Maybe it's nevertheless helpful. Let me begin my attempt at answering your question with a distinction ...

View answer
Fault-tolerant programming languages / paradigms?
Accepted answer
9 votes

A good place to start looking for work coming from the PL community could be the following. Joe Armstrong's work on Erlang, see e.g. his PhD thesis. This work continues to have a profound influence ...

View answer
Category-theoretic treatment of diffs, patches and merging?
8 votes

There is quite a bit of work in this direction. You could start by looking at [1, 2], but they don't exhaust the topic. S. Mimram, C. Di Giusto, A Categorical Theory of Patches. C. Angiuli, E. ...

View answer
Formal semantics of tactics
Accepted answer
8 votes

I'm not sure this answers your question, but the first (?) paper on the subject of tactics appears to have been Milner's The Use of Machines to Assist in Rigorous Proof.

View answer
Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?
8 votes

I agree with Alexis and Damiano, and there is another dimension to $\lambda$-calculus that is not often emphasised, because of the dominance of the Curry-Howard correspondence in thinking about the $\...

View answer
Church-Rosser property for dependently typed lambda calculus?
8 votes

Quite a bit is know about this. The concept of Pure Type Systems (PTS) is useful for showing Church-Rosser (CR) for large classes of typed $\lambda$-calculi. Paraphrasing (1): PTS with only β ...

View answer
Can choice or sequential execution be expressed with other basic operators of the pi calculus?
Accepted answer
8 votes

This is a really interesting question and only partially understood. The $ \newcommand{\OUT}[2]{\overline{#1} #2 } $ precise answer to such questions depends in subtle ways on exactly what the ...

View answer
How to introduce recursion to Simply Typed Lambda Calculus while at the same time keeping strong normalisation?
Accepted answer
8 votes

Which of the following are you asking: are there ways of enriching the simply-typed $\lambda$-calculus with mechanisms (presumably by restricting the available forms of recursion) such that exactly ...

View answer
Formal Semantics of Programming Languages
8 votes

Structural operational semantics (SOS) is a very general concept. It's essentially just a binary relation on configurations (usually programs plus a context, like state, or available continuations), ...

View answer
List of (unsolved) complexity problems arising from PL
Accepted answer
7 votes

Pippenger's (1) from 1996 shows that (under some assumptions) strict (CBV) functional programming languages are asympotically slower than imperative languages. It is open whether Pippenger's result ...

View answer
Determinism and pi-calculus
Accepted answer
7 votes

There are plenty such typing systems. Most work is based on the linear/affine typing system introduced in (1) and generalised in (2). Here are the main works on this subject. In (3) the typing system ...

View answer
Fixed points in computability and logic
7 votes

I'm probably not directly answering your question, but there is a common mathematical generalisation of a lot of paradoxa, including Gödel's theorems and the Y-combinator. I think this was first ...

View answer
How to measure programming language succinctness?
7 votes

The ideas the question expresses are interesting but maybe insufficiently fleshed out. I can see a couple of points that deserve further refinement. It is difficult to "code the exact same ...

View answer
Resources (books, etc) to learn about concurrency theory
Accepted answer
6 votes

There are not that many books on this subject, as it continues to evolve at a rapid pace. Classic books on process calculi (that don't focus on π-calculus-like mobility) are: C. A. R. Hoare, ...

View answer
Is simply typed lambda calculus equivalent to primitive recursive functions
Accepted answer
6 votes

The simply-typed λ-calculus with β-equality at type (o → o) → o → o (which can be seen as type of the natural numbers, whenever o is any base type) can define exactly the extended polynomials (= ...

View answer
"Impredicative" in type theory
6 votes

The definition of an object $X$ is impredicative, if the definition uses a collection $C$ in the construction of $X$, such that $X$ is a member of $C$. So impredicativity is a form of circularity. ...

View answer
How to prove relations between "classes" of types?
6 votes

One approach to such questions is via encodings. Say you have a language $L_1$ and a language $L_2$ and you want to show that they are somehow "the same", you can do this by finding an encoding $$ ...

View answer
In what fields does a knowledge of formal semantics prove useful?
6 votes

Formal semantics is useful primarily when you want to reason about programs. In the past this was mainly done in programming language development (and to a lesser degree in compiler construction). ...

View answer
Well-formedness condition for inductive types
6 votes

Inductive types have been studied heavily and many variants exist. A well-known introduction to inductive definitions is P. Aczel, An Introduction to Inductive Definitions which was originally ...

View answer
How is duality of types defined?
6 votes

In my experience, a good and operational way to understand duality of types for $\lambda$-calculi is by going through $\pi$-calculus. When you translate (decompose) types into process calculus, ...

View answer
What are the differences between logical relations and simulations?
6 votes

I'd say that the two concepts are somewhat vague. Both are about binary relations of computational mechanisms which somehow embody a notion of equality. Logical relations are defined by induction of ...

View answer
Full Completeness vs Full Abstraction of a program translation
5 votes

Summary: full completeness means that the interpretation function is not just complete, but also surjective on programs. Full abstraction has no requirement for surjectivity. $\newcommand{\semb}[1]{...

View answer