# Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

324 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
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 ...
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.
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
994 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, ...
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, ...
9k 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?
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 ...
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:...
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 ...
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 ...
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?
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 ...
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 ...
2k 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 ...
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 ...
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 ...
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?...
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 ...
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 ...
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 ...
3k views

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) ...
823 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)$ ...
1k 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?
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?)
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 ...
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 ...
925 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 ...
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 ...
829 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 ...
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 ...
490 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 ...
2k views

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$ ...
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 ...
817 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 ...
2k views

### Status quo of category theory and monads in theoretical computer science research?

Background. I am a bachelor student who is interested in research related to category theory, monads and Haskell, and I want to find a topic for my bachelor’s thesis in that area. I have looked at ...
384 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 ...
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 :...