Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

5
votes
3answers
4k views

Why isn't it possible to recover/resume after an Exception?

I know that Exceptions as a means of flow-control is generally frowned upon. But in my opinion, Exceptions have little value short of the flow-control aspect - after all, if you didn't want the ...
13
votes
1answer
266 views

Relationship between shift-reduce parsing and delimited continuations?

Has anyone formalized the relationship between shift-reduce parsing techniques and delimited continuations? When constructing a bottom-up parser (eg, LR parsers), we take a grammar and then ...
16
votes
1answer
619 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 ...
15
votes
1answer
3k views

How does inheritance differ from subtyping?

In programming language perspective, what is mean by subtyping? I heard that "Inheritance is not Subtyping". Then what are the differences between inheritance and subtyping?
29
votes
1answer
908 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, ...
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) ...
3
votes
2answers
337 views

Confusing (to me) statement from “Type Classes in Haskell”

I'm reading up on type classes, and started looking at the paper Type Classes in Haskell. In Section 2.2 - Superclasses, the authors use the following example: ...
20
votes
5answers
887 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 ...
2
votes
0answers
134 views

Recursion Schemes for Static Analysis (AST)

In the process of creating an AST analysis framework one of the challenges is creating good reusable functions and to avoid too much boiler-plate code. To that end catamorphisms seem like a good fit, ...
10
votes
6answers
2k views

Removing recursion - a look into theory behind the scenes

I am new to this site and this question is certainly not research level - but oh well. I have a little background in software engineering and almost none in CSTheory, but I find it attractive. To make ...
5
votes
2answers
373 views

(concise?) definition of thread safety

Wikipedia has the following definition: Thread safety is a computer programming concept applicable in the context of multi-threaded programs. A piece of code is thread-safe if it only ...
4
votes
5answers
401 views

Advantages and specific applications of massively parallel programming thesis idea

I'm nearly graduated in computer science engineering and my thesis should discuss the massively parallel computational model of CUDA and its advantages/applications. I'm searching for an application ...
2
votes
2answers
475 views

Are register based machines on von neumann architecture diametrically opposed to functional programming style?

We are so used to von neumann architecture and say a register machine like the x86. (Also with programming languages built for those machines x86 assembly, C, etc) Is that approach to computing ...
6
votes
2answers
398 views

Reynolds: “the basic laws of variable binding”

I recently came across this passage in an article by John Reynolds (emphasis added): ...from designers innocent of the principles of programming language design, we have been given a nearly endless ...
3
votes
3answers
311 views

Automatic proofs or model checking in an extremely simplified functional language

Imagine a stripped down functional programming language, that has the following properties The only value type is an integer There are no side effects Functions are defined as a single expression, ...
28
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 ...
3
votes
2answers
343 views

Does using Normal Order Evaluation instead of Normal Order Reduction lose the Normalization theorem?

Normal Order Reduction (NOR) reduce the leftmost, outermost redex. Normal Order Evaluation (NOE) reduce the leftmost, outermost redex, but not within the body of abstractions. So (λw. (λx.x) z) is ...
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?)
32
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 ...
12
votes
6answers
2k views

Functions that typed lambda calculus cannot compute

I just want to know some examples of the functions that can be computed by the untyped lambda calculus but not by typed lambda calculi. As I am a beginner, some reiteration of background information ...
13
votes
4answers
738 views

Modeling objects (OOP) in dependent type theory

I am interested in modeling objects, from object oriented programming, in dependent type theory. As a possible application, I would like to have a model where I can describe different features of ...
1
vote
1answer
821 views

What do people mean by capabilities and capacities?

Someone made a casual remark to me about the terminology of capabilities and capacities, in the context of threads, processors and runtime systems, particularly their theoretical modelling. For ...
6
votes
1answer
373 views

Term that can distinguish beta-equivalent normal forms in the untyped lambda calculus

I'm trying to work through two (non-assessed) class-work questions and am stuck on a question that seems similar to one I could do. The first question was to prove that there does not exist a $\...
4
votes
2answers
344 views

Parametric equation in pi-calculus

This is the first time I ask a question on cstheory, so I am very sorry for my english. I have a (maybe very trivial) problem when trying to find a well-form representation for a root of a recursive ...
8
votes
2answers
272 views

Is there any work done on developing difference-calculus of Turing Machines (or simpler Formal Languages)

I am attempting to develop some notions of a difference-calculus between a notional Ideal Turing Machine conceived by a developer (e.g. whatever is intended by a software developer), call it $M_I$, ...
15
votes
3answers
803 views

When can we say that two programs are different?

Q1. When can we say that two programs (written in some programming language like C++) are different? The first extreme is to say that two programs are equivalent iff they are identical. The other ...
7
votes
3answers
1k views

What are the relationships between Functional Reactive Programming, Automatic Differentiation, Self-Adjusting Computation and Partial Evaluation?

Self-adjusting computation seems to be related to all of the other topics, but I would like to get a clearer sense of how they all relate. For example, do any of them subsume or obsolete any of the ...
6
votes
3answers
541 views

Boolean as subtype of integer

In languages oriented towards systems programming, digital logic and hardware design, it's common to treat boolean as a subtype of integer. In languages oriented towards mathematics and type theory, ...
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 ...
3
votes
0answers
214 views

Understanding the goals you can reach with different programming models and languages

I come to ask this question here, because Meta told me this place was probably best for it. Reference: https://meta.stackexchange.com/questions/114043/ I've read this article many a times and ran in ...
9
votes
2answers
317 views

Research on call-site based type inference?

I'm trying to learn more about whole-program type checking and type inferencing systems that use information from function call sites to compute type information (in addition to the standard approach ...
-3
votes
3answers
582 views

In what manner and to which degree would programming on a hypothetical ternary computer differ than from binary computers?

To expound upon my question as mentioned in the title, I am researching, out of curiosity, what the implications of a (balanced) ternary based computer would be, besides obvious things such as greater ...
7
votes
1answer
1k views

Fault-tolerant programming languages / paradigms?

I've been passively thinking for a long time, what could be the foundation for programming systems that can tolerate their own and other systems' bugs (not even speaking of environmental conditions ...
7
votes
2answers
812 views

Closed term and alpha-conversion

In the simply-typed lambda calculus, do we ever need alpha-conversion in a small-step call-by-value reduction of a term that is closed? The evaluation rule that uses substitution is: $(\lambda x.t_1)~...
10
votes
3answers
2k views

Type inference for imperative statements other than assignment

In my search for research papers about type systems for imperative languages, I only find solutions for a language with mutable references but without genuine imperative control structures such as ...
4
votes
2answers
149 views

finding constantness of a term

Let $S$ be a multisorted algebraic signature with function symbols $f_0, f_1, \ldots$. For every $i$, I partially know “constantness” of $f_i$. (I have no precise definition of constantness yet.) ...
3
votes
2answers
211 views

A question in constraint based analysis

I may have a very naive question on Constraint Based Analysis. (a technique of static program analysis). I am reading an informal introduction from F. Nielson He gives such an example, ...
7
votes
2answers
294 views

Simple model of computation with homoiconicity

Is there a simple model of computation with homoiconicity? It would also be nice if, like beta reduction in lambda calculus, every step in execution yields a new valid program. Besides the lack of ...
22
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 ...
15
votes
2answers
380 views

Proof theory of biproducts?

A category has biproducts when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts? Perhaps the best-known example is the ...
8
votes
2answers
239 views

Where can I find an elementary small-step structural operational semantics for closures?

Lexical closures are an implementation technique in languages with first-class functions. I'm interested in a simple operational description of function closures. Does anyone know of such a ...
0
votes
1answer
145 views

Lengths and substitution in L-systems

Am looking into writing up a Lindenmayer systems implementation. I've looked at a few example implementations and the one thing that's giving me trouble at this stage is how symbols and substitutions ...
-6
votes
3answers
331 views

How can I call functions that are not “first-class functions”?

I mean, is there an antonym for "first-class function"?
2
votes
2answers
752 views

Equivalence of two basic blocks

My questions: What are other names for this and similar problems and their fields? ("equivalence of varieties in universal algebra", "equivalence of algebraic structures", "rewriting systems for ...
-3
votes
1answer
313 views

Did someone give a formal definition of normal and applicative order?

In all courses and textbooks I have seen, normal order reduction (NOR) and applicative order reduction (AOR) are defined as reducing respectively the leftmost outermost and rightmost innermost redex. ...
5
votes
2answers
389 views

the type system does not tell the whole story due to “exception”

I am wondering whether it is a bad style to use "exception". For example, in Ocaml, the exception does not appear as the .mli file. So it appears to me that "exception" is something that cannot be ...
10
votes
1answer
165 views

Reference for the undefinability of modulus of continuity functional in PCF?

Can someone point me to the reference for the non-definability of the modulus of continuity functional in PCF? $\newcommand{\N}{\mathbb{N}}$ $\newcommand{\bool}{\mathsf{bool}}$ Andrej Bauer has ...
13
votes
2answers
428 views

What are the equational laws for zero types?

Disclaimer: while I care about type theory, I don't consider myself an expert on type theory. In the simply typed lambda calculus, the zero type has no constructors and a unique eliminator: $$\frac{\...
15
votes
2answers
824 views

What is the origin of logical relations?

I actually have two questions: Who first used logical relations to relate semantics? I traced them back to Reynold's "On the Relation Between Direct and Continuation Semantics", but I can't claim to ...
4
votes
1answer
886 views

Why have computer scientists chosen recursor instead of iterator in primitive recursion?

I wonder why computer scientist have chosen recursor instead of iterator (or tail recursor if you like) in primitive recursion, given that function defined in terms of iteration behaves more ...