Share Your Experience: Take the 2024 Developer Survey

# Tag Info

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 ...
• 161k
Accepted

• 1,866
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. ...
• 12.1k
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 ...
• 14.6k

### 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 ...
• 81.8k

### 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 ...
• 3,704

### 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 ...
• 2,516

### 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 ...
• 987

### 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 &...

### 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 ...
• 659
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)....
• 277k
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 ...
• 29.8k
Accepted

### Quantifiers in lambda calculus

It appears that the author is using lambda notation for sets and relations. That is, sets are represented as boolean-valued unary functions, and relations are represented as boolean-valued binary (or ...
• 14.6k
Accepted

### The importance of the language semantics for code generation and frameworks for code generation in model-driven development

In general when we talk about code generation (or model-to-model transformation in general), clearly defined semantics is quite important, since such transformations usually make sense when both the ...
• 540