Programming languages, in particular, focussing on their semantics.

learn more… | top users | synonyms (2)

0
votes
1answer
33 views

How to specify and verify Horn clauses (logic programming programs)? Semantics of Horn clauses

There are lot of applications of Horn clauses (notable examples include use of rules in cognitive architectures and knowledge bases, as well as use of rules in business rules programs). Are there ...
6
votes
1answer
92 views

Confusions about the technique for verifying implementations of linearizable objects in [Herlihy and Wing, 1990]

In Section 4.3.2 entitled "Proof Method" of Herlihy and Wing, "Linearizability: A Correctness Condition for Concurrent Objects", 1990 the authors describe the technique for verifying ...
13
votes
2answers
1k 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 ...
9
votes
1answer
116 views

Logical Reations for an Impredicative System in a Predicative MetaTheory

Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in ...
1
vote
1answer
132 views

Is my language Turing-complete?

Consider a language like Brainfuck but without the brackets. At the end of each line (i.e. when "\n" occurs), if the current cell is not 0, then the line is re-executed. An example of an infinite ...
2
votes
0answers
33 views

How can unification be applied to interaction combinators?

The problem of unifying interaction combinators is probably undecidable since those are turing complete. As opposed to the lambda calculus, there is nothing like a simple type theory for interaction ...
4
votes
1answer
63 views

How can you encode natural numbers operations on interaction combinators?

The church-encoding for natural numbers is a natural mean of implementing addition, multiplication and so on on the lambda calculus. Interaction nets are said to be an alternative universal ...
7
votes
2answers
163 views

What's the difference between reduction strategies and evaluation strategies?

From the evaluation strategy article on Wikipedia: The notion of reduction strategy in lambda calculus is similar but distinct. From the reduction strategy article on Wikipedia: It is ...
14
votes
4answers
440 views

Program reasoning about own source code

The inspiration for this question is the following (vague) question: What are the programming language/logical foundations for having an AI which could reason about its own source code and modify it? ...
7
votes
1answer
214 views

An example where smallest normal lambda term is not fastest

Let the $size$ of $\lambda$-terms be defined as follows: $size(x) = 1$, $size(λx.t) = size(t) + 1$, $size(t s) = size(t) + size(s) + 1$. Let the complexity of a $\lambda$-term $t$ be defined as ...
4
votes
1answer
46 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 ...
2
votes
1answer
80 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
155 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
282 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
236 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 ...
3
votes
1answer
107 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
82 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
201 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
149 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
118 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
156 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
144 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
441 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
91 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
149 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 ...
15
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
298 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
253 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
159 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
177 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
455 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
102 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
114 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
103 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
151 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
314 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
147 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
92 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
87 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
159 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
145 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 ...
2
votes
0answers
148 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
244 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
556 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
183 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
219 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
174 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
141 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
548 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 ...