25 votes
Accepted

What is this fraction-like "discrete mathematics"–style notation used for formal rules?

This is a standard notation for an inference rule. The premises are put above a horizontal line, and the conclusion is put below the line. Thus, it ends up looking like a "fraction", but with one or ...
D.W.'s user avatar
  • 156k
13 votes
Accepted

What questions can denotational semantics answer that operational semantics can't?

There is no real agreement what characterises denotational semantics (see also this article), except that it must be compositional. That means that if $\newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \...
Martin Berger's user avatar
13 votes
Accepted

Break keyword outside a loop is syntax error or semantic error?

Both work, so how you do it is up to you. But there are a couple of reasons to consider doing it during a post-parse analysis: While it is certainly possible to define two different types of ...
rici's user avatar
  • 11.9k
10 votes
Accepted

Is reference counting GC vs. tracing GC a language property or an implementation property?

Swift guarantees that once the last reference to an object is dropped the object is deinitialized, and the deinit code is immediately run. Obtaining this kind of ...
chi's user avatar
  • 14.4k
10 votes
Accepted

What's the difference between a calculus and a programming language?

The meaning of the words is not fixed, but I can give you my interpretation. A calculus is something that we calculate with in the sense of juggling equations (think manipulation of Taylor series or ...
Andrej Bauer's user avatar
9 votes

Why do some authors not include summation in the $\pi$-Calculus?

To answer this question, it's best to reflect on the meaning of sums in process calculi. Essentially sums express a lack of knowledge. The process $P + Q$ means something along the lines of "either $P$...
Martin Berger's user avatar
9 votes

What is a predicate transformer?

The predicate transformer is just a formalization of the idea that you can produce a precondition given a program and its postcondition. For example, given a program ...
chepner's user avatar
  • 209
9 votes
Accepted

What formal representation is commonly used to describe compiler optimizations?

There are many compilers, which compile widely different kinds of languages which serve widely different purposes. For example, a database language will have very different optimizations than an array-...
cody's user avatar
  • 8,114
8 votes

When would one use equational dynamics?

What you call "equational dynamics" is not actually an operational semantics, it's an equational theory. As you note, equations by themselves do not tell us how to run programs. However, they are ...
Andrej Bauer's user avatar
8 votes
Accepted

Programming language semantics prototyping tool

Although there are frameworks created specifically for the purpose of prototyping programming languages (including their semantics, type systems, evaluation, as well as checking properties about them),...
ivcha's user avatar
  • 540
8 votes
Accepted

What does it mean to "strengthen the precondition and weaken the postcondition" in Hoare logic?

Condition $A$ is stronger than condition $B$ if $A$ implies $B$. That is, if $B$ holds in all situations in which $A$ holds. Conversely, if $A$ is stronger than $B$, then $B$ is weaker than $A$. ...
David Richerby's user avatar
8 votes

Formal model of execution for Java (or general imperative language)

There is an (operational) semantics for Java 1.4 formulated in the $\mathbb{K}$ framework. Associated to this framework is a proof system called Matching Logic. While that page describes a prototype ...
Derek Elkins left SE's user avatar
8 votes
Accepted

What is meant by a full abstract model of a lambda-calculus like language?

In denotational semantics, you want to be able to map each of your language terms to some object in your semantic domain or model. Now, it cannot be any arbitrary domain/model as you like, but, ...
Apoorv's user avatar
  • 659
8 votes

Is type-checking "syntactic" or "semantic"?

Although I personally would describe type analysis as semantic, this question seems to start with the assumption that there is a clear, formally-definable dividing line between "syntax" and "semantics"...
rici's user avatar
  • 11.9k
7 votes

What is this fraction-like "discrete mathematics"–style notation used for formal rules?

Here is a very informal explanation that might help people unfamiliar with formal notations to get a foot in the door. It does not replace a formal definition! The Ap is the state of your system or ...
trunklop's user avatar
  • 171
7 votes
Accepted

Formal model of execution for Java (or general imperative language)

Featherweight Java is quite highly regarded in the PL community. But if that doesn't suit your needs, here's a general approach to modelling: Formalize your language's AST into expressions and ...
jmite's user avatar
  • 29.7k
6 votes

Typing dependent pattern matching

In general matching with dependent types can be quite subtle! You'll note that in the Coq documentation that the extended pattern-matching syntax is ...
cody's user avatar
  • 8,114
6 votes

Why injection into sum type apparently leads to ambiguity?

I think the key point here is $\sigma$, $\tau$ and $\phi$ are type variables, and not specific types. So, what the typing rule for $\operatorname{inl}$ says is that $\operatorname{inl} M$ is of type $\...
svick's user avatar
  • 1,866
6 votes

denotional semantic for while - fixed points

Your proposed alternate definition is no good. It tries to define $[[\text{while b do S}]]$ in terms of $[[\text{while b do S}]]$. That's a circular definition: you can't define something in terms ...
D.W.'s user avatar
  • 156k
6 votes

What questions can denotational semantics answer that operational semantics can't?

I'll write $O(p,\sigma)$ for the only $\sigma'$ so that $\langle p, \sigma \rangle \to \sigma'$ (and $\bot$ if it doesn't exist) and $D(p)$ for the denotational semantics of $p$. Note that if you ...
xavierm02's user avatar
  • 1,245
6 votes
Accepted

How to express modalities in lambda calculus - are some extensions required?

Are extensions required? Not really. You can take an axiomatic description of a modal logic and simply provide a "primitive" lambda term for each. The modal operators would become type constructors. ...
Derek Elkins left SE's user avatar
6 votes
Accepted

What's the difference between: operational, denotational and axiomatic semantics?

I think your examples show you do somehow understand the basic points of the several styles of semantics. Still, note that the whole point of having a semantics of a programming language is to have a ...
chi's user avatar
  • 14.4k
5 votes

What kind of formal semantics can describe HTML and CSS?

I think the paper "Automated Reasoning for Web Page Layout" might be interesting to you. This paper defines CSS semantics in order to verify the layout formally. Look at section 3 of the paper for ...
nekketsuuu's user avatar
5 votes

Does the closure of a function include the actual parameter passed to the function?

No. A closure is a function, and, as such, its parameters are passed when the function is called. The main difference between closures and plain functions is that closures are associated with an ...
Mario Cervera's user avatar
5 votes

How does recursion works when there are 2 or more consecutive recursive calls?

Just like any other two consecutive statements in an ordinary programming language, they're executed one after the other. However, since the two recursive calls operate on disjoint sections of the ...
David Richerby's user avatar
5 votes

Quantifiers in lambda calculus

There is no notion of quantification in the standard $\lambda$-calculus as introduced by Church. As far as I can tell from Liang's paper, it deals with a specialized version of $\lambda$-calculus in ...
Hans Hüttel's user avatar
  • 2,486
5 votes

Is type-checking "syntactic" or "semantic"?

(From my limited experience) I would certainly call type-soundness a semantic property of a program, rather than a syntactic one. In some dynamic languages (e.g., lisp, python sans type annotations &...
D. Ben Knoble's user avatar
5 votes

What should I read to understand semantics of programming languages?

There are many depending on where you want to start and what exactly you want. Usually textbook start with giving semantics to the While or ...
Apoorv's user avatar
  • 659
5 votes
Accepted

Relation between programming languages requiring declaration of variables before use and using the token class $\text{id}$ while parsing

In order for their example to work, the authors need identifiers to be of unlimited length. This is because the language $$ \{ wcw : w \in \{a,b\}^*, |w| \leq n \} $$ is context-free (indeed, regular)....
Yuval Filmus's user avatar
5 votes
Accepted

Resources for implementing dependent type theory

This paper is my go-to for implementing dependent types. It starts from the basics, uses bidirectional types, and has accompanying code in Haskell. If you're at all interested in type inference, this ...
jmite's user avatar
  • 29.7k

Only top scored, non community-wiki answers of a minimum length are eligible