Episode #125 of the Stack Overflow podcast is here. We talk Tilde Club and mechanical keyboards. Listen now

Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

Filter by
Sorted by
Tagged with
103
votes
7answers
8k views

Solid applications of category theory in TCS?

I've been learning a few bits of category theory. It certainly is a different way of looking at things. (Very rough summary for those who haven't seen it: category theory gives ways of expressing all ...
67
votes
7answers
3k views

Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

Mathematicians sometimes worry about the Axiom of Choice (AC) and Axiom of Determinancy (AD). Axiom of Choice: Given any collection ${\cal C}$ of nonempty sets, there is a function $f$ that, given a ...
48
votes
12answers
3k views

What is the theoretical basis of imperative programming?

Functional programming has a theoretical basis in lambda calculus and combinatory logic. As someone involved with statistical computing, I find these concepts to be very useful for modeling. Is ...
45
votes
7answers
6k views

What constitutes denotational semantics?

On a different thread, Andrej Bauer defined denotational semantics as: the meaning of a program is a function of the meanings of its parts. What bothers me about this definition is that it doesn't ...
43
votes
7answers
3k views

Using lambda calculus to derive time complexity?

Are there any benefits to calculating the time complexity of an algorithm using lambda calculus? Or is there another system designed for this purpose? Any references would be appreciated.
37
votes
7answers
6k views

What do we know about provably correct programs?

The ever increasing complexity of computer programs and the increasingly crucial position computers have in our society leaves me wondering why we still don't collectively use programming languages in ...
35
votes
8answers
2k views

Higher-order algorithms

Most of the well-known algorithms are first-order, in the sense that their input and output are "plain" data. Some are second-order in a trivial way, for example sorting, hashtables or the map and ...
35
votes
6answers
5k views

Regular expressions aren't

Ask even someone with a background in computer science what a regular expression is, and the answer is likely to go beyond the constraint of being within reach of a finite-state automaton. For ...
33
votes
3answers
2k views

Type classes vs object interfaces

I don't think I understand type classes. I'd read somewhere that thinking of type classes as "interfaces" (from OO) that a type implements is wrong and misleading. The problem is, I'm having a problem ...
32
votes
5answers
2k views

Programming languages for efficient computation

It is impossible to write a programming language that allows all machines that halt on all inputs and no others. However, it seems to be easy to define such a programming language for any standard ...
32
votes
4answers
15k views

Research and open challenges in Programming Language Theory

In the spirit of some general discussions like this one, I'm opening this thread with the intention to gather opinions on what are the open challenges and hot topics in research on programming ...
31
votes
7answers
7k views

Books on programming language semantics

I've been reading Nielson & Nielson's "Semantics with Applications", and I really like the subject. I'd like to have one more book on programming language semantics -- but I really can get only ...
31
votes
4answers
2k views

Relationship between contracts and dependent typing

I've been reading some articles on dependent types and programming contracts. From the majority of what I've read, it seems that contracts are dynamically checked constraints and dependent types are ...
29
votes
3answers
2k views

Curry-Howard and programs from non-constructive proofs

This is a follow up question to What is the difference between proofs and programs (or between propositions and types)? What program would correspond to a non-constructive (classical) proof of the ...
29
votes
4answers
3k views

What are the differences between logical relations and simulations?

I'm a beginner working on methods proving program equivalence. I've read a few papers about defining logical relations or simulations to prove two programs are equivalent. But I am quite confused ...
29
votes
1answer
930 views

Programming languages with canonical functions

Are there any (functional?) programming languages where all functions have a canonical form? That is, any two functions that return the same values for all set of input is represented in the same way, ...
28
votes
6answers
2k views

Why naturals instead of integers?

I'm interested in why natural numbers are so beloved by the authors of books on programming languages theory and type theory (e.g. J. Mitchell, Foundations for programming languages and B. Pierce, ...
28
votes
5answers
8k views

What are some good introductory books on type theory?

I'm recently studying Haskell and programming languages. Could someone recommend some books on type theory?
28
votes
4answers
6k views

What is the most powerful kind of parser?

As a side-project, I'm writing a language using Python. I started by using a flex/bison clone called Ply, but am coming up against the edges in the power of what I can express with that style of ...
28
votes
6answers
2k views

Maximum computational power of a C implementation

If we go by the book (or any other version of the language specification if you prefer), how much computational power can a C implementation have? Note that “C implementation” has a technical meaning:...
27
votes
6answers
9k views

What is the difference between propositions and judgments?

I get confused by the subtle difference between propositions and judgments when exposed to intuitionistic type theory. Can any one explain to me what is the point to distinguish them and what ...
27
votes
2answers
4k views

What is the logarithm or root operation in type-space?

I was recently reading The Two Dualities of Computation: Negative and Fractional Types. The paper expands on sum-types and product-types, giving semantics to the types ...
26
votes
5answers
1k views

What is the difference between proofs and programs (or between propositions and types)?

Given that the Curry-Howard Correspondence is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?
25
votes
5answers
2k views

Are there any annotated formal verification systems for pure functional programming languages?

ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified. I have not looked into it, but I imagine that the ...
25
votes
3answers
3k views

What's the difference between term rewriting and pattern matching?

As there was no response at Lambda the Ultimate I try it here again: term rewriting systems are used for instance in automated theorem proving a symbolic calculation, and of course to define formal ...
25
votes
2answers
1k views

Context Sensitive Grammars and Types

1) What, if any, is the relationship between static typing and formal grammars? 2) In particular, would it be possible for a linear bounded automaton to check whether, say, a C++ or SML program was ...
24
votes
6answers
2k views

How should I think about proof nets?

In his answer to this question, Stephane Gimenez pointed me to a polynomial-time normalization algorithm for proofs in linear logic. The proof in Girard's paper uses proof nets, which are an aspect of ...
24
votes
2answers
1k views

Do dependent types give you everything subtyping does?

Types and Programming Languages focuses quite a bit on subtyping, but as far as I can tell, subtyping doesn't seem especially fundamental. Does subtyping give you anything more than dependent types do?...
23
votes
10answers
2k views

For a language to be programmable, is it mandatory that it be based on a context free grammar

Practically, for a language that can eventually be compiled/transformed into system level instructions, is it necessary that it be a context free grammar? ex: Are all programming/scripting languages ...
23
votes
2answers
1k views

Is there an expressiveness hierarchy for type systems?

Inspired by the extensive hierarchies present in complexity theory, I wondered if such hierarchies were also present for type systems. However, the two examples I've found so far are both more like ...
23
votes
4answers
2k views

When does (or should) Theoretical CS care about intuitionistic proofs?

From what I understand (which is very little, so please correct me where I err!), theory of programming languages is often concerned with "intuitionistic" proofs. In my own interpretation, the ...
23
votes
2answers
1k views

What is the folk model of linear logic?

Probably the most common application of linear types in PL is to use them to give languages which control aliasing (i.e., a linear value has a single pointer to it, more or less). But there's a ...
22
votes
2answers
801 views

Can the cost of GC be neglected when analyzing the running time of worst-case data structures specified in a garbage-collected programming language?

I just realized that I have been assuming the answer to my question is "yes" but I don't have a good reason. I imagine that maybe there is a garbage collector that provably introduces only $O(1)$ ...
22
votes
1answer
977 views

How are Futures described in terms of category theory?

Is there a useful description of futures or promises in terms of category theory? In particular, what could the categorical dual of Future be?
22
votes
1answer
1k views

Class of functions computable by Coq

Since it does not allow nonterminating computation, Coq is necessarily not Turing-complete. What is the class of functions that Coq can compute? (is there an interesting characterization thereof?)
21
votes
2answers
3k views

What's the difference between ADTs, GADTs, and inductive types?

Might anyone be able to explain the difference between: Algebraic Datatypes (which I am fairly familiar with) Generalized Algebraic Datatypes (what makes them generalized?) Inductive Types (e.g. Coq) ...
20
votes
7answers
1k views

How can we know that formal methods work?

An important goal of formal methods is to prove the correctness of systems, either by automated or human-directed means. However, it seems that even if you can give a correctness proof, you may NOT be ...
20
votes
5answers
897 views

Compiler correctness proofs

I am looking for tutorial material that covers compiler correctness proofs, preferably using denotational methods, at the level of a beginning grad student. Alternatively, do you know of some ...
20
votes
2answers
2k views

Has the semantics of TeX (as a programming language) ever been formalized?

It seems to me that the macro language employed by $\TeX$ can maybe be seen as some kind of term rewriting system or some kind of programming language with call-by-name scoping. Even modern ...
19
votes
2answers
2k views

What are the limits of total functional programming?

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 ...
19
votes
1answer
785 views

Scott's stochastic lambda calculi

Recently, Dana Scott proposed stochastic lambda calculus, an attempt to introduce probabilistic elements into (untyped) lambda calculus based on a semantics called graph model. You can find his ...
18
votes
6answers
1k views

Which models of computation can be expressed through grammars?

This is a reformulation of Are grammars programs? previous asked by Vag and with many suggestions from the commenters. In what way can a grammar be seen as specifying a model of computation? If, for ...
18
votes
3answers
466 views

Frame rule as a change-preserver?

A frame rule, like the one given below, captures the idea that, given a program c with precondition p that holds before it runs ...
18
votes
2answers
2k views

Implicit vs explicit subtyping

This page asserts that many languages do not use implicit subtyping (structural equivalence), prefering explicit/declared subtyping (declaration equivalence) I've mostly used programming ...
17
votes
3answers
780 views

Formal Semantics of Programming Languages

I'm new to programming languages theory and I'm seeking for a good resource on a resource for formal semantics of programming languages. Specifically looking for structural operational semantics. I ...
17
votes
3answers
2k views

Reader, Writer monads

Let $C$ be a CCC. Let $(\times)$ be a product bifunctor on $C$. As Cat is CCC, we can curry $(\times)$: $curry (\times) : C \rightarrow(C \Rightarrow C)$ $curry (\times) A = \lambda B. A \times B$ ...
17
votes
1answer
340 views

List of (unsolved) complexity problems arising from PL

What are some major, open computational complexity problems that arise from programming languages, especially program analysis and compilation? I am looking for problems on the lines of "the time ...
16
votes
3answers
566 views

Is there any programming language theory describing foreign function interfaces (FFI) and multiple language bindings?

Is there any programming language theory describing foreign function interfaces (FFI) and multiple language bindings? I have asked some implementation issues on stackoverflow, which is not suitable ...
16
votes
3answers
1k views

What is the role of predicativity in inductive definitions in type theory?

We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A :...
16
votes
1answer
623 views

(How) can you model broadcasts in the pi-calculus?

Can you model reliable broadcasts in the pi-calculus? If so: How? If not: Are there any similar process algebras where you can? What I have tried: If sender $S$ wants to send a message $y$ to ...