Questions tagged [pl.programming-languages]
Programming languages, in particular, focussing on their semantics.
375
questions
2
votes
3
answers
239
views
References on model checking and pi calculi
I'm a mathematician and it looks like I need to learn about these topics. What would be good references that go into the technical details of the following topics?
(s)pi calculus
model checking
I'm ...
- 21
2
votes
1
answer
129
views
How to auto-derivate sequential iterative programs from a mathematical specification?
I had to derivate, by hand, sequential iterative programs at school using an unified Hoare-Dijkstra-Hehner programming theory.
First, write down the formal specification as a Hoare triple and figure ...
- 23
2
votes
2
answers
236
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,
...
- 265
2
votes
1
answer
175
views
What graphs on $\mathbb{N}$ can be encoded as regular languages?
Suppose I represent the natural number 0 by "x", and use the symbol "s" for successor so that I get the following encoding of $\alpha : \mathbb{N} \rightarrow V$ of natural numbers ...
2
votes
1
answer
494
views
programming language with type-level functions
Is there any programming language out there that allows the same set of tools it offers, to be used at the type level as well? I know, Haskell and some other ML family languages allow parametric types ...
- 123
2
votes
1
answer
294
views
Damas-Milner-like subset of the calculus of constructions with global type inference
Damas-Milner is a subset of System Fω that gives up expressivity (type-level computation) for usability (type inference). The experience with Haskell and ML attests to the practical value of this ...
- 501
2
votes
2
answers
251
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 ...
- 167
2
votes
2
answers
330
views
A few questions about ISWIM
I recently read Landin's paper "The Next 700 Programming Languages". But I was a bit confused by ISWIM. In particular, are functions first-class objects in ISWIM? It seems not because every ...
- 2,805
2
votes
2
answers
303
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 ...
- 409
2
votes
1
answer
1k
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 ...
- 175
2
votes
1
answer
101
views
Conditional Dependencies in Compiler Semantic Analysis Passes
Imagine that we have a been given an Excel spreadsheet with three columns, labeled COND, X and Y.
...
- 369
2
votes
1
answer
90
views
Nominal Tree Languages i.e. with Binders and Infinite Symbols?
I'm wondering if there has been any research done into automata that accept languages of trees that can bind arbitrary variables, and are considered equal under alpha equivalence.
I've found so far:
...
- 2,832
2
votes
1
answer
120
views
Completeness of Constraint Typing (type inference) question regarding $\sigma'$
The theorem of completeness of type inference states the following:
Suppose $\Gamma \vdash t:S| _{\mathcal{X}}C$,
...
- 185
2
votes
1
answer
466
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 ...
- 141
2
votes
1
answer
252
views
A few questions about Object-Oriented Languages in general
I was not a big fan of Object-Oriented Languages (OOL), but recently started to learn a bit more about their pros and cons in a general setting instead of diving into one such language. I have a few ...
- 2,805
2
votes
1
answer
177
views
Intuitive way to handle variable binding
Suppose we have an algebraic datatype parameterised by a type variable name, e.g.
...
2
votes
1
answer
163
views
Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook
I am working through the Dependent Types chapter from Advanced Topics in Types and Programming Languages (ATTAPL) by Benjamin Pierce et al. I am confused with the calculus presented Fig 2-7 (Calculus ...
- 31
2
votes
0
answers
99
views
Is there a relationship between Brown and Palsberg's Self-Interpreter for F-Omega and Lawvere's Fixed Point Theorem?
Brown and Palsberg [0] demonstrated an self-interpreter for F-Omega. To do so, they perform "a careful analysis of the classical theorem [of the impossibility of self-interpretation by total ...
- 81
2
votes
0
answers
74
views
Reference request: characterisation of simultaneous substitution
For simply typed λ-calculus, a simultaneous substitution from $\Gamma$ to $\Delta$ is concretely a type-preserving map from variables in $\Delta$ to terms in $\Gamma$. See, for example, Programming ...
- 121
2
votes
0
answers
303
views
Are CCS and CSP still worth studying?
In Winskel's The formal semantics of programming languages 1993, Ch14 Nondeterminism and parallelism says
This chapter is an introduction to nondeterministic and
parallel (or concurrent) ...
- 639
2
votes
0
answers
78
views
Is there a list of notations developed for regular expressions? [closed]
There is, of course, PCRE.
I know also of Olin Shiver's Structural Regular Expressions, and Rob Pike's Structural Regular Expressions.
I also understand that Raku's regexps are different from perl's ...
- 121
2
votes
0
answers
83
views
Categorical model of binding / first class modules
Binders are explained using presheaves (Pitts/Gabbay A new approach to Abstract Syntax with variable binding)
What is the equivalent (categorical) theory to explain first class modules as in 1ML ?
- 121
2
votes
0
answers
176
views
Is there is an intuitive explanation why call-by-name PCF is less expressive than both call-by-value PCF and lazy PCF?
J.C. Mitchell cites in his "Expressive power of programming languages" the result in Riecke's "Fully abstract translations between functional languages" about the call-by-value, call-by-name and lazy ...
2
votes
0
answers
106
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 ...
- 2,329
2
votes
0
answers
203
views
Evaluation contexts: outside-in vs inside-out
I heard that there exist two styles to define an evaluation context: outside-in and inside-out. Can someone give the definitions? Why are they so named (inside-out and outside-in)? What is the ...
- 2,805
2
votes
0
answers
183
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, ...
- 121
1
vote
3
answers
633
views
Is there an array structure that allows for O(1) complexity for reverse, zip, slice etc operations?
Many operations on arrays have $O(n)$ complexity.
If we represent arrays as accessors methods, many of them could be done in $O(1)$. For example, the $i$th item in the reverse of an array $A$ of ...
- 3,137
1
vote
2
answers
223
views
Is there a computation class describing FOR-programs, what are the limitations?
I've written an unpublished paper that describes FOR-programs.
FOR-programs are programs that only contain bounded for loops and basic operations (assignment, addition, multiplication, etc.). A ...
1
vote
3
answers
391
views
Is there a common mathematical symbology for collections?
Preface: So, it was suggested in 'Programmers' that I ask this over here.
I am being asked to define several of my algorithms in mathematical terms to describe my work to a customer. I trying to ...
- 21
1
vote
1
answer
147
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 ...
- 409
1
vote
2
answers
205
views
Can concurrency models be compared in terms of some metrics?
In Seven Concurrency Models in Seven Weeks by Butcher, it compares Actor Model and Communicating Sequential Processes (CSP):
CSP is more flexible than actor model:
In actor model, the medium of ...
- 639
1
vote
1
answer
218
views
What relations and differences are between formal semantics for linguistics and for programming languages?
I browsed the table of content of Cann's Formal Semantics, which reminds me of the things that I saw in programming language books.
Cann's book is for linguistics, and am I right that it is helpful ...
- 639
1
vote
1
answer
208
views
Is data structure necessarily a functor?
The justification of my conjecture is that (seemly) any data structure can have a mapper that applies a given function $f$ to each element of the structure. A data structure in the end is a container ...
- 111
1
vote
1
answer
98
views
Extension of primitive recursion, that is as powerful as System-T
I know that System-T restricted to first-order types is exactly as powerful as primitive recursive functions, because I proved it in Agda.
I asked myself, if there is a extension of primitive ...
1
vote
2
answers
168
views
Automated transformation into spigot algorithm?
Is there any research on transforming 'standard' algorithms into spigot algorithms?
I'd be happiest with automated transformations, but happy to learn about any research in this area.
For my ...
- 111
1
vote
1
answer
2k
views
How to recognize safe queries in tuple relational calculus?
How do I determine whether query in tuple relational calculus is a safe query?
- 111
1
vote
1
answer
279
views
Algebraic effects and handlers, dynamic effects
What exactly are dynamic effects? What does it mean to dynamically create an effect?
In a language with algebraic effects and handlers (such as Eff or Koka) one could already do different operations ...
- 701
1
vote
1
answer
618
views
Verification: how 'formal' is a tool like Java Modeling Language (JML) compared to certified libraries and model checking?
(note: this is probably a beginner question, and English is not my first language)
Recently, I have read a paper that used the “Java Modeling Language” (JML), see for instance:
http://www.eecs.ucf....
- 443
1
vote
1
answer
153
views
Observational Equivalence of open terms in PCF
The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms.
Lets consider the simple case where the terms ...
- 31
1
vote
4
answers
1k
views
A simple programming language?
What is a simple toy research programming language that has simple denotational semantics (including numbers or reals) that is used often to demonstrate certain properties of programming languages, or ...
- 31
1
vote
1
answer
251
views
Parallel programming languages which look deterministic? [closed]
Are there any programming languages where the system parallelizes the program without any noticeable differences for the programmer?
That is, the programmer writes a linear, deterministic program, ...
- 199
1
vote
1
answer
848
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 ...
- 11
1
vote
0
answers
83
views
Abstract domain monad
I was reading old lecture from a CS course at Cornel and I have some doubts about the following at 2.4
It defines how to transform domains between each other via a Galois Insertion, more formally:
...
- 11
1
vote
0
answers
73
views
Is it possible to define beta reduction for PHOAS?
I'm using Parametric Higher-Order Abstract Syntax (PHOAS) as a representation for untyped lambda calculus in OCaml:
...
- 105
1
vote
0
answers
94
views
Alternative notions of bisimulation
Suppose $(S, \Lambda, \rightarrow)$ is a labeled transition system. A bisimulation is a relation $R \subseteq S \times S$ s.t. $\forall \alpha \in \Lambda$ and $\forall p, q \in S$ with $R(p,q)$,
$\...
- 11
1
vote
0
answers
81
views
Decision vs search problem specification
Let us suppose we have a sort function.
One way of specifying it is to say that a sort function is any function where if the input/output are vectors $I, O$, then $O_i \leq O_j \forall i < j$ and ...
- 1,311
1
vote
0
answers
34
views
Non Turing-Complete Models, Conditional-Complete function?
I know well the distinction between the class of Partial Recursive Functions, and $\mu$-Recursive, i.e. the latter is Turing Complete and the former is equivalent to the LOOP-Program model of ...
1
vote
0
answers
57
views
How to justify this causally consistent execution in the $(vis, ar)$ framework for distributed consistency models?
In Figure 5.1 of the book "Principles of Eventual Consistency" by Sebastin Burckhardt, 2014, Causal Consistency (CC); wiki is (mainly) defined as the conjunction of $hb \subseteq vis$ and $hb \...
- 2,329
1
vote
0
answers
111
views
Confusion about the visibility and arbitration relations in a formal framework for distributed consistency models
In the POPL'14 paper "Replicated Data Types: Specification, Verification, Optimality" and the book "Principles of Eventual Consistency", the authors propose a formal framework for ...
- 2,329
1
vote
0
answers
188
views
Definitions of strongest postconditions [closed]
The weakest precondition of while loop $\mathtt{while}(G)\{C\}$ with respect to postcondition $P$ can be characterized by the least fixed point of the predicate transformer
$X ~\mapsto \neg G \wedge ...
- 81