Programming languages, in particular, focussing on their semantics.

learn more… | top users | synonyms (2)

-2
votes
0answers
65 views

How does one elegantly add new programming language features without bootstrapping? [closed]

Main question: How does one elegantly add new programming language features without bootstrapping? Background This is a fairly multi-faceted question, so I thought it would be useful to give some ...
4
votes
1answer
41 views

Is infinitary Böhm-reduction wrt. root-active terms for $\lambda$-calculus transitive?

I expect the answer to be "obviously yes", but to my inexperienced eye, that's not directly obvious, because the definition of infinite Böhm-reduction does not include a transitivity rule (it wouldn't ...
1
vote
1answer
63 views

Is there a pair of different lambda terms in the normal form that behave identically when applied to any input?

Let f and g be lambda terms in the normal form, such that f is intensionally different from ...
3
votes
1answer
129 views

Actual practical example of a prefix-free Turing-complete language

A theoretical construct that comes up a lot in algorithmic computability theory is a universal prefix-free language. For my purposes, this is a language with the following properties: its syntax is ...
7
votes
3answers
207 views

For what languages is there already a theory of observational equivalence?

For a correctness proof, I'm looking for a usable notion of program equivalence $\cong$ for Barendregt's pure type systems (PTSs); missing that, for enough specific type systems. My goal is simply to ...
3
votes
3answers
210 views

Distinguishing semantics vs syntactic techniques and the syntax of your semantic domains

Consider a denotational semantics from simply-typed $\lambda$-calculus into dependent type theory. Is that actually a (trivial) term transformation into that dependent type theory? After all, type ...
2
votes
1answer
88 views

Can type inference be classified in two groups: unification-based and control-flow-based?

I recently came across the 1995 paper Safety analysis versus type inference (pdf link) by Palsberg and Schartzbach that contrasts unification-based type inference and static analysis methods based on ...
4
votes
1answer
71 views

In which posets is the set of compact elements downwards closed?

In a poset $(D, \sqsubseteq)$, a compact element is an element $d \in D$ such that for every directed set $A$ which happens to have a supremum $\bigsqcup A \in D$ with $d \sqsubseteq \bigsqcup A$, it ...
10
votes
1answer
181 views

Reference for the fact that (0=1) implies false requires a universe in MLTT

It's a fairly well-known fact that deriving a contradiction from a disequality (for example, $(0=1) \to \bot$) in Martin-Loef type theory requires a universe. The proof is also fairly ...
2
votes
2answers
133 views

What is the formalism behind ?- (query) in Prolog?

I am in general interested in a more formal (better be logical, as in related to mathematical logic) definition of a query. As an example, there's Prolog operator ...
0
votes
0answers
108 views

Is there an algorithm to find whether 2 combinators form a Turing-complete system?

It is known that K = (λx.(λy.x)) and S = (λx.(λy.(λz.((x z) (y z))))) define a turing complete system, and we know procedures to ...
0
votes
2answers
126 views

Converting a Hardware description language to a functional programming language [closed]

I am looking for some guidelines on converting a Hardware description language such as VHDL or Verilog to a Typed Language. The reason I want to do this is to formally verify a hardware whose ...
1
vote
1answer
124 views

understanding programming monads through diagrams

I am trying to understand better how the category definition of monad is related to the computer science definition. nlab has a rather terse definition of Monad in terms of a bicategory. an object ...
13
votes
1answer
338 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 ...
23
votes
5answers
1k 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 ...
3
votes
0answers
80 views

How to analyze the quality of data definition language? [closed]

I know that DDL is most often used when talking about databases, but I see no reason why XML, PDF or even to some extent Prolog shouldn't belong to this category. It looks like branches of CS ...
6
votes
2answers
123 views

Call-by-push-value's denotational semantics of “thunk diverge”

I was reading about Call-by-Push-Value in the introducing paper from 1999, but I have some confusion, partially because of my unfamiliarity with domain theory. I might have figured it out, but I'd ...
13
votes
5answers
2k 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?
6
votes
1answer
295 views

Describing state machines mathematically

The short paper "Computer Science and State Machines" by Leslie Lamport seems quite strange to me. On the one hand, I am surprised to see that an important hardware protocol called "two-phase ...
5
votes
1answer
232 views

Type theory for memory safe data structures

Data structures such as a doubly linked list and a B+ tree have blocks of memory that have multiple pointers to it. This creates the risk that a bug will allow memory to be accessed after being freed. ...
3
votes
2answers
148 views

What requirements should a denotational semantics for a programming language satisfy to be correct?

We have a programming language and its denotational semantic, like Tony Hoare's CSP with its syntax and denotational semantic e.g. stable failure and UTP. We want to extend the language (its ...
5
votes
0answers
158 views

Generalizing Haskell: could we replace Hask with Cat?

N.B. I asked the same question on Stack Overflow but it was suggested that it is too theoretical for this forum. It is great that Haskell allows us to walk around in the category $Hask$. But ...
5
votes
1answer
434 views

Is this behavior in a programming language inconsistent?

I'm developing a tiny programming language to try to wrap my head around type inference, and I'm trying to figure out if its behavior makes sense or not. Here's the problem: The identity function ...
8
votes
1answer
95 views

Hypersequents: proof term assigments or translations to hybrid logic

I've been looking at a modal logic with the axiom $$ (\Diamond A \land \Diamond B) \to \Diamond((A \land \Diamond B) \vee (A \land B) \vee (A \land \Diamond B)) $$ Roughly, this says that the ...
6
votes
1answer
109 views

A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2

I'm having a problem regarding Theorem 5.4.40.3 of Barendregt's Lambda calculi with types (1992), a chapter in Handbook in logic in computer science. (I'm referring to the PostScript version available ...
7
votes
0answers
96 views

What is known about reduction by “$P_1$ interprets $P_2$” for generalized programming languages?

Inspired by this answer, let's say that a programming language is given by the data $L=(P,ev)$ where $P$ (the set of "valid programs") is a computable subset of $\Sigma^*$ and $ev$ (the "evaluator") ...
5
votes
2answers
139 views

Is there a mathematical analysis/proof available for correctness of solutions to inter process communication problems?

I've been going over some material related to IPC recently from Tanenbaum's "Modern Operating Systems" and revisited semaphore after many years. There is a lot of code and pseudo code based ...
6
votes
4answers
203 views

Use of Process Calculi and PL Theory for modern programming language development

For a while now, I have been very interested in programming language theory and process calculi and have started to study them. To be honest, it something that I wouldn't mind going into for a career. ...
7
votes
1answer
139 views

Are there stronger notions of equivalence over lambda terms than beta equivalence?

I should add the context that I am concerned with strongly normalizing systems like System-F. I have what I consider a very strong notion of equivalence for lambda terms that goes something like the ...
3
votes
1answer
88 views

Is it possible to determine if a reduction is correct?

Suppose we have an arbitrary term, x, in Lambda Calculus, or in an equivalent turing-complete system. Suppose we ask an oracle what is the normal form of that term, ...
1
vote
0answers
81 views

Object-Oriented Programming Languages based on assignment

Is it correct to claim that an object-oriented programming language based on assignment (e.g., Java and Smalltalk) introduces mutability and hence complexity in concurrent applications ? In other ...
2
votes
2answers
156 views

Would it be possible for a compiler to convert a recursive sum into the average formula?

def sum1(n): if n==0: return 0 else: return n + sum1(n-1) def sum2(n): return n*(n+1)/2 A compiler can not convert ...
2
votes
0answers
138 views

How useful is program search in the field of programming-language theory?

I've been thinking: computing systems such as the Lambda Calculus and its variations are usually very simple and can be implemented in as few as ~80 lines of Haskell code. There is a self-interpreter ...
1
vote
0answers
115 views

Is there any system where function equality (extensionality) is decidable?

Is there any programming language or system where function equality (extensionality) is decidable?
10
votes
0answers
237 views

A bijection between ordered lambda terms and rooted planar maps?

Consider the following recurrence in two parameters $n$ and $k$: \begin{aligned} NF(0,k) &= 0 \\ NF(n,k) &= Neu(n,k) + NF(n-1,k+1) \\ Neu(n,k) &= [n=1 \wedge k=1] + ...
4
votes
4answers
455 views

How to introduce recursion to Simply Typed Lambda Calculus while at the same time keeping strong normalisation?

Suppose you have a version of the STLC with one base type, similar to: data Tree = Branch Tree Tree | Leaf Now, suppose you want to add recursion to that ...
7
votes
0answers
166 views

Is there a programming language where any arbitrary recursive function can be fused?

Compilers like GHC for Haskell use inlining as one of its most important optimising tools. Doing that is not possible for recursive functions, in general. A few techniques have been developed to amend ...
6
votes
0answers
191 views

Complete combinator basis for System F-omega

The S and K combinators form a complete (and Turing complete) basis when untyped. Within the Hindley-Milner type-system, and I believe within system $F$ as well, S and K can encode any well-typed ...
2
votes
1answer
132 views

Language with extensible type system?

Is there a practical programming language that has an extensible type system? Or alternatively, an add-on type system that can be used with existing languages? With extensible I mean that the typing ...
7
votes
1answer
124 views

Decidability of inductive invariant existence in Presburger arithmetic

Problem: Consider a finite number of control states (including an "initial" and a "bad" state), a finite number of integer variables, and for each ordered pair of states a transition relation ...
5
votes
1answer
454 views

How can I prove formally semantic equivalence of programming languages?

I would like to compare two languages which are from different programming paradigms. Both langauges are object oriented languages, but one of them a multiparadigm language because it supports ...
3
votes
2answers
109 views

Well-formedness condition for inductive types

I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. ...
9
votes
1answer
248 views

Algorithm to determine function equality on the simply typed lambda calculus?

We know that beta-equality of simply typed lambda-terms is decidable. Given M,N:σ→τ, is it decidable whether for all X:σ, MX $≃_β$ NX?
12
votes
1answer
299 views

Can we distinguish strictly syntactic and semantic methods in programming language?

While discussion strong normalization proofs, this comment contrasts the "normal forms model" with "purely syntactic methods". This brings me back to a more basic question: can we still distinguish ...
9
votes
1answer
157 views

Program Minimization

Circuit Minimization is the problem to minimize the size of a given circuit. Is there anything similar for general programs? In particular my question is - Do there exist algorithms to minimize the ...
4
votes
1answer
134 views

Is it possible to create an algorithm-aware optimizer?

I've recently implemented a physics system where each object has to interact with eachother. It consisted of, pretty much, the following algorithm: ...
1
vote
1answer
311 views

What's the relation between OOP and category theory?

What's the relation between OOP and category theory? Is there some related work on this topic one can read?
1
vote
2answers
127 views

Tool for specifying operational semantics for given formally specified programming language

I am trying to translate code from one programming language into another (to be specific - from RuleML to Drools, but other pairs can be expected as well) and it would be nice to know - whether there ...
2
votes
0answers
43 views

Are the sets of executions of data-race free programs equal, when run on causal memory and on sequentially consistent memory respectively?

In the paper "Causal Memory: Definitions, Implementations, and Programming (Distributed Computing [DC] 1995)", the authors present a formal definition of causal memory, an abstraction of distributed ...
1
vote
1answer
171 views

How can an inherited attribute be simulated using a synthesized attribute?

Is it possible to simulate an inherited attribute using a synthesized attribute? For example, can the inherited attribute SYMTAB used in normal code generation modules be simulated using a synthesized ...