14,360 reputation
3474
bio website andrej.com
location Slovenia
age 44
visits member for 4 years, 10 months
seen 17 hours ago

I am a professional mathematician and theoretical computer scientist (what is the difference?) . My area of work is a mix of logic, semantics, programming languages, category theory, constructive mathematics and computability.


2d
revised Information-theoretic Diffie-Hellman
Fix the world's worst abuse of LaTeX ever.
Jul
2
comment Smallest possible universal combinator
Maybe this is of interest: wolframscience.com/nksonline/page-1123a-text?firstview=1
Jun
12
comment Why do non-proper types have no terms?
Type operators are clearly not types, unless you stretch the meaning of "type" beyond anything reasonable. They are functions from types to types. Why you call them improper types in your class I do not know.
Jun
12
comment Why do non-proper types have no terms?
Isn't this what I said? Pair is a function at the kind-level and should not be treated as a type (but rather as a type operator, in other words a function). The reason you are treating type operators as types is probably pedagogical (I am guessing). Why don't you ask prof. Pierce?
Jun
11
comment In homotopy type theory, is there a IsManifold predicate?
Types in homotopy type theory are like $(\infty, 1)$-objects.
Jun
11
revised Why do non-proper types have no terms?
added 811 characters in body
Jun
11
answered Why do non-proper types have no terms?
Jun
11
comment In homotopy type theory, is there a IsManifold predicate?
In homotopy type theory the types should be thought of as homotopy types. Thus you would need a homotopy-theoretic characterization of those homotopy types that arise as the homotopy types of manifolds. Is there one?
Jun
3
comment Counterintuitive results for undergraduates
Agreed, but it's the sort of ourageous theorem that sparks people's interest. It gives them a jolt and makes them doubt their own intuitions about infinity.
May
28
awarded  Nice Answer
May
27
revised A total language that only a Turing complete language can interpret
added 4 characters in body
May
27
comment Is there a general theory for why certain algorithms are inefficient in high-level languages?
When a variable is declared it must be initialized. Instead of null introduce option types and make sure with good syntax than whenever anyone uses a value of option type they check both possibilities (undefined and defined).
May
27
awarded  Nice Answer
May
26
revised Counterintuitive results for undergraduates
added 1028 characters in body
May
26
revised Counterintuitive results for undergraduates
added 1028 characters in body
May
26
answered Counterintuitive results for undergraduates
May
26
comment What do we know about provably correct programs?
"Provably" is misused here several times but it's not your fault. Computer scientists do it all the time. You do not mean "provably correct programs" but presumably "programs whose correctness has been proved".
May
20
comment Categorical way of factoring out points
It's not clear to me at all why you need categories, and in any case your definition of the category is not clear, how does composition work, where do identity morphisms come from? Also, I think I do not understand the terminology. If the objects of your category are literals, then how can an implication $a_i \leftarrow L_i$ be a morhism when $L_i$ is a conjunction of several literals? At best this could be a multicategory, or there's something basic I misunderstand here.
May
18
comment Actual practical example of a prefix-free Turing-complete language
@EmilJeřábek: you're right about adding digits in an arbitrary way. But we can save the day and require that every computable way of adding more digits to a string eventually produces a valid program (because König's lemma fails by Tarski's unbouded computable tree that has no computable infinite path).
May
15
comment Categorical way of factoring out points
Could you say a bit more about how your categorical semantics works so far. What is $\Pi$ in the semantics, an object? Why do you need categories anyway? Can't you just do everything with sets?