Martin Berger
  • Member for 11 years, 4 months
  • Last seen this week
How does type theory change how one thinks about programming?
3 votes

"Types are the leaven of computer programming; they make it digestible." Robin Milner

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
Difference between statically and dynamically typed languages
2 votes

The question is subtle and simple at the same time, hence deep. Let me give you a simplifying answer. First you need to realise there there three somewhat orthogonal distinctions which are often ...

View answer
What is the "question" that programming language theory is trying to answer?
15 votes

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

View answer
Feel dissatisfied after each submission
4 votes

By the time we submit the paper, I am so dismayed that results in the paper seem almost trivial. I'd argue that you had failed to solve the problem if it didn't seem trivial after completion! The ...

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
Equivalent formulation of complexity theory in Lambda Calculus?
Accepted answer
16 votes

As you point out, the λ-calculus has a seemingly simple notion of time-complexity: just count the number of β-reduction steps. Unfortunately, things are not simple. We should ask: Is counting β-...

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
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
What is the intuition behind linear logic?
Accepted answer
11 votes

I'm not sure this question is ideal for CSTheory, but given that it's already gathering upvotes, here is an answer somebody might have given had the question been posted on cs.stackexchange. In ...

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
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
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
Encoding an infinitely looping process with state in the pi-calculus
3 votes

The process $P{\langle 0, c, d\rangle}$ in the context of a recursively defined process like $$ P{\langle count, c, d\rangle} \quad\stackrel{\text{def}}{=}\quad c(v).(\overline{d}\langle count+v ...

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
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
Asymptotic complexity of CDCL SAT solver that only selects negative literals
3 votes

Not a direct answer to the question but, as DPLL can be seen as a special case of CDCL, hopefully of interest. The problem of finding optimal branching literals for DPLL is (in a way) harder than SAT ...

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
"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
Sequential execution in π-Calculus
2 votes

Sequential execution is an edge case of concurrent computation. Robin Milner said this clearly in his Turing award lecture "Elements of interaction" (CACM, 36(1), 1993): I reject the idea that there ...

View answer
Semantic equivalence using a model of computation of two languages
Accepted answer
2 votes

Let me clarify the setting, which has nothing to do with $\pi$-calculus or bisimulation. The first thing you have to realise that it does not make much sense to talk about a programming language ...

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
What are the negative consequences of extending CIC with axioms?
4 votes

A practical example of an axiom behaving badly you ask, what about this? 0 = 1 The Coquand paper referred to might be [ 1 ], where he shows that dependent ITT (Martin-Löf's intuitionistic type ...

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
Book for self study of algorithms in group theory
4 votes

Not a book but maybe A. Hulpke's Notes on Computational Group Theory are of interest?

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
History of recursion
3 votes

Maybe slightly tangential to the original question, but the blog entry "How recursion got into programming: a comedy of errors" describes an interesting part of early computing history.

View answer
Scope of active substitutions in the applied $\pi$-calculus
3 votes

The key to understanding scope management in $\pi$-calculi is to look at the structural congruence $P \equiv Q$ and at the notions of free name $\newcommand{\FN}[1]{\text{fn}(#1)}\FN{P}$ and free ...

View answer
Universal and existential types
1 votes

I suggest not to give up on the operational intuition. Operational is primary, all semantics are derived, and are but proof techniques for operational semantics. The key ideas are as follows. A ...

View answer