Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

Filter by
Sorted by
Tagged with
3 votes
1 answer
248 views

Why would the term "dynamically typed" be considered a misnomer?

In the book "Types and Programming Languages", the author writes: The word "static" is sometimes added explicitly - we speak of a "statically typed programming language",...
Léo Vital's user avatar
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 ...
Antonio Caruso's user avatar
4 votes
1 answer
475 views

Areas of research and open problems in functional programming [closed]

What are the major areas of functional programming that require more research and development? For example, I know a lot of people are asking for dependent types in Haskell, and someone at my uni is ...
otah007's user avatar
  • 141
3 votes
0 answers
156 views

Set:Set or Negative Inductives in a Total Language?

In total dependently typed languages, general recursion is forbidden, since this can allow for non-terimination. However, dependently typed language can still describe Turing-complete computations (...
Joey Eremondi's user avatar
3 votes
0 answers
127 views

Equational Theories for Type Systems

I was reading through Gunter's Semantics of Programming Languages: Structure and Techniques and in the second chapter on simply typed $\lambda$ calculus he introduces an equational theory with $\beta\...
Apoorv's user avatar
  • 141
2 votes
1 answer
162 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 ...
Ram's user avatar
  • 31
0 votes
0 answers
98 views

Proposition terms vs types in Coq

Consider the following div function written in Coq. It takes in a proof that the divider is non-zero. Definition div (n d:nat) (pf: ~(d = 0)) := n/d. Focus on <...
Ram's user avatar
  • 31
-1 votes
1 answer
76 views

Chomsky-Schutzenberg Hierarchies explained for physicist (general) [closed]

I am classically trained in physics, however I have been interested in the use of information theory in studying some classical systems. As someone who is somewhat unfamiliar with the language of ...
user54963's user avatar
9 votes
3 answers
483 views

Can Non-termination be considered an algebraic effect?

Non-termination is sometimes considered an effect. I have been reading about algebraic effect systems (What is algebraic about algebraic effects and handlers?), and I suspect non-termination (like ...
user833970's user avatar
6 votes
1 answer
169 views

Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?

To perform type inference in the presence of polymorphic recursion, one can use a Kleene-Mycroft iteration to compute the principal type of an expression. To type $\mathsf{fix}\ f\ldotp e$, we define $...
Joey Eremondi's user avatar
3 votes
1 answer
164 views

Verified type checkers

Most of the work on programming language metatheory mechanization focus on the declarative properties of the languages (e.g., type soundness), but fail to address the algorithmic side, i.e. the type ...
xrq's user avatar
  • 1,175
12 votes
2 answers
1k views

Applications of algebraic geometry in type theory/programming language theory

Lately, I have become interested in algebraic geometry and have started reading on it. I still know very little about this field, but I do want to know if it has any connection with my main field, ...
xrq's user avatar
  • 1,175
0 votes
1 answer
346 views

Where does a C-like language without heaps belong in the automata hierarchy?

Assume that the language C', unlike C, has well-defined semantics, but has similar features: pointers and manual memory management through malloc and free. Assume that C'' is the same as C' without ...
Abhishek's user avatar
12 votes
1 answer
4k views

What is the "question" that programming language theory is trying to answer?

I've been interested in various topics like Combinatory Logic, Lambda Calculus, Functional Programming for a while and have been studying them. However, unlike the "Theory of Computation" which ...
PhD's user avatar
  • 5,275
0 votes
0 answers
99 views

How to get started with program synthesis

I am a CS Major, I am a programmer with 10 years of experience. i want to get to know about program synthesis. there are no video tutorials / courses available online. i have researched about Emina ...
cypher's user avatar
  • 117
12 votes
2 answers
754 views

Intuition Behind Strict Positivity?

I'm wondering if someone can give me the intuition behind why strict positivity of inductive data types guarantees strong normalization. To be clear, I see how having negative occurrences leads to ...
Joey Eremondi's user avatar
1 vote
0 answers
54 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 \...
hengxin's user avatar
  • 2,329
4 votes
2 answers
528 views

Extending Hindley-Milner to type mutable references

I have been trying to implement a programming language from scratch, and have gotten reasonably far. It reads just like Python, other than the fact that let is used ...
Enrico Borba's user avatar
1 vote
0 answers
110 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 ...
hengxin's user avatar
  • 2,329
11 votes
1 answer
892 views

How to tell if an effect is algebraic?

I've read Bauer's What is algebraic about algebraic effects and handlers? and he talks about IO being an algebraic effect, even though it doesn't have any equations. In other papers on algebraic ...
Jesper Dahl's user avatar
4 votes
0 answers
118 views

Proof that CIC or Dybjer-style eliminators are strongly-normalizing?

Related to this question I'm wondering, what is the standard technique for showing that dependent types with eliminators are strongly normalizing? I'm thinking something like the Calculus of ...
Joey Eremondi's user avatar
5 votes
1 answer
210 views

Is F<: with bottom undecidable?

We all know that F<: is undecidable: http://www.cse.chalmers.se/~abela/lehre/SS07/Typen/pierce93bounded.pdf However, I have difficulties finding that anyone claiming the version with bottom added ...
Jason Hu's user avatar
  • 251
4 votes
0 answers
169 views

Hereditary Substitution with Inductives and Eliminators?

I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators? In particular, normalizing the application of an eliminator to an ...
Joey Eremondi's user avatar
7 votes
1 answer
508 views

Busy Beaver Equivalent for the Untyped Lambda Calculus

In the same way that the Busy Beaver function is defined for Turing Machines, we could define a similar function for the untyped lambda calculus: Over all terms in the ULC composed of ...
isaacg's user avatar
  • 806
11 votes
2 answers
446 views

Hereditary substitution with a universe hierarchy

I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types. I'm wondering, are there any examples of hereditary substitution in ...
Joey Eremondi's user avatar
6 votes
2 answers
299 views

Typing of substitution in a bidirectional type system

In most typed lambda calculi, we have the following lemma: If $\Gamma \vdash t_1 : \tau_1$ and $\Gamma, x : \tau_1, \Delta \vdash t_2 : \tau_2$ then $\Gamma,\Delta[t_1/x] \vdash t_2[t_1/x] : \tau_2[...
Joey Eremondi's user avatar
6 votes
2 answers
440 views

Preservation under Substitution with Telescopes

In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution": If $\Gamma \vdash v : \tau_1$ and $(x : \tau_1) \vdash t : \tau_2$, then $\Gamma \...
Joey Eremondi's user avatar
6 votes
2 answers
128 views

Formal semantics of tactics

Tactics are supposed to represent inference rules in a system, and it might seem unnecessary at first to formalize the semantics of tactics; nevertheless, modern theorem provers can have pretty ...
xrq's user avatar
  • 1,175
12 votes
1 answer
970 views

Proof techniques for showing that dependent type checking is decidable

I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and ...
Joey Eremondi's user avatar
7 votes
3 answers
342 views

Why/when do we ever need transfinite loop variants?

I do not understand why one would ever need a transfinite loop variant. Why do natural-number-valued variants not suffice? My simple (but perhaps too naive) argument is: if a loop $L$ terminates ...
blk's user avatar
  • 81
13 votes
5 answers
606 views

Representing bound variables with a function from uses to binders

The problem of representing bound variables in syntax, and in particular that of capture-avoiding substitution, is well-known and has a number of solutions: named variables with alpha-equivalence, de ...
Mike Shulman's user avatar
5 votes
1 answer
234 views

Confusion about a formal definition of PRAM consistency

I am reading the paper "Consistency in Non-Transactional Distributed Storage Systems" by Paolo Viotti and Marko Vukolić. The authors provide a comprehensive survey of various consistency semantics ...
hengxin's user avatar
  • 2,329
6 votes
3 answers
474 views

Sorting a programs instructions until it works

Lets say I have a computer program below. (define (factorial x) (if (= x 0) 1 (else (* x (factorial (- x 1))))) I then take each line of the ...
Joshua Herman's user avatar
0 votes
1 answer
816 views

What is the practical importance of making or using a Turing complete language? [closed]

I get what a Turing machine is and what language is a Turing-complete language but when someone introduces me to a new programming language (like Solidity) and says it is Turing complete, what am I ...
n0unc3's user avatar
  • 19
5 votes
2 answers
224 views

Does Standard ML validate (CBV) eta equivalence?

$\eta$ equality of functions is fundamental in their Category-theoretic semantics but in practice even "functional" languages include "impure" features that violate it. Note that this is not an issue ...
Max New's user avatar
  • 1,675
7 votes
4 answers
7k views

Difference between syntax and semantic error in programming languages

When compilers generate errors for a specific programming language, there's distinction between syntax & semantic errors. E.g. ) + f 3 has ill-formed syntax, ...
Rui Liu's user avatar
  • 181
8 votes
1 answer
108 views

Question on subtyping of handlers in "An Effect System for Algebraic Effects and Handlers"

I had a question on subtyping in the paper "An Effect System for Algebraic Effects and Handlers". I was wondering why there isn't a subtyping rule for adding effects on both sides of a handler type, ...
Labbekak's user avatar
  • 701
3 votes
1 answer
134 views

Escaping references in Eff and resources

In the paper "Programming with Algebraic Effects and Handlers" there is the issue where references (dynamic instances of a state effect, defined using algebraic effects) can propagate outside the ...
Labbekak's user avatar
  • 701
7 votes
1 answer
464 views

Avoiding Cycles with Unification and Subtyping

Context I realize that subtyping often doesn't admit principle types, and that inference in the presence of subtypes is undecidable. I'm working in a context where typechecking should simply fail ...
Joey Eremondi's user avatar
2 votes
1 answer
491 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 ...
Sam R.'s user avatar
  • 123
21 votes
2 answers
2k views

Has the semantics of TeX (as a programming language) ever been formalized?

It seems to me that the macro language employed by $\TeX$ can maybe be seen as some kind of term rewriting system or some kind of programming language with call-by-name scoping. Even modern ...
Nicola Gigante's user avatar
17 votes
1 answer
511 views

List of (unsolved) complexity problems arising from PL

What are some major, open computational complexity problems that arise from programming languages, especially program analysis and compilation? I am looking for problems on the lines of "the time ...
xrq's user avatar
  • 1,175
0 votes
1 answer
179 views

Language/type system closest to Haskell without general recursion

I've implemented a completely functional DSL, and now I'd like to reason about it. It would be helpful to be able to compare it to existing languages. The type system is parametric polymorphic with ...
lightning's user avatar
  • 433
18 votes
3 answers
1k views

Type-based memory safety without manual memory manage or runtime garbage collection?

Let's say we wanted a typeful, pure functional programming language, like Haskell or Idris, that is aimed at systems programming without garbage collection and has no runtime (or at least not more ...
analogyschema's user avatar
2 votes
2 answers
210 views

How can you state how abstract interpretation gets around Rice's Theorem succinctly?

At this question, abstract interpretation has a nice in-depth look. However, I'd like someone to clearly and very precisely state how abstract interpretation takes the result of Rice's Theorem over ...
CinchBlue's user avatar
  • 309
1 vote
1 answer
272 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 ...
Labbekak's user avatar
  • 701
2 votes
0 answers
82 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 ?
nicolas's user avatar
  • 121
1 vote
0 answers
187 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 ...
blk's user avatar
  • 81
4 votes
1 answer
138 views

Questions about algebraic effects and handlers, decomposed handlers

Can a handler always be decomposed? Say a handler for Get and Set effects could be decomposed to a handler for Get and a handler for Set. After they could be composed again by first applying the ...
Labbekak's user avatar
  • 701
3 votes
2 answers
296 views

Languages that lack contraction, weakening or exchange

When learning about generalized arrows, a question arised to me: Are there any languages (or potential languages) that lack one or more of the structural rules: contraction, weakeing and exchange? ...
Petr's user avatar
  • 2,581

1
2
3 4 5
8