10,235 reputation
2152
bio website andrej.com
location Slovenia
age 42
visits member for 3 years, 7 months
seen 2 days 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.


Apr
17
revised What does consistency mean for “computational theories” corresponding to inductive types?
added 1 character in body
Apr
17
comment What does consistency mean for “computational theories” corresponding to inductive types?
There are various ways of expressing inconsistency, but they all amount to "the system is trival". In type theory one kind of inconsistency is "every type is inhabited", which in the presence of an empty type (primitive or derived) is the same as "the empty type is inhabited". Note however that there are perfectly interesting type theories with inhabited types, e.g., programming languages with recursion. Konstantin, you speak of other kinds of inconsistencies, and we keep asking you what they might be. Can you please be concrete? What more do you want than to inhabit every type?
Apr
17
revised What does consistency mean for “computational theories” corresponding to inductive types?
added 876 characters in body
Apr
17
answered What does consistency mean for “computational theories” corresponding to inductive types?
Apr
17
awarded  Enlightened
Apr
16
awarded  Nice Answer
Apr
16
comment Homotopy type theory and Gödel's incompleteness theorems
My point was that people do not expect a perfect transportation machine to exist, and neither do they worry that there isn't one, but somehow they worry about the fact that no (reasonable) foundation of mathematics is complete.
Apr
16
answered Homotopy type theory and Gödel's incompleteness theorems
Apr
15
revised What is logic programming and does it really add anything new to the logic?
deleted 2 characters in body
Apr
14
answered What is logic programming and does it really add anything new to the logic?
Apr
14
comment How to write the introduction of a research paper?
Now that you mention it, all papers of mine that included photos of kittens were accepted, too.
Apr
14
answered How to write the introduction of a research paper?
Apr
7
awarded  Nice Answer
Apr
2
reviewed Approve suggested edit on Theta functions of automata relations
Apr
2
comment Example of where violation of strict positivity condition in inductive types leads to inconsistency
Yeah, I just realized that. My example doesn't hold water.
Apr
2
comment Example of where violation of strict positivity condition in inductive types leads to inconsistency
I am thinking $\mu \alpha . (\alpha \to 2) \to \alpha$ should be pretty bad.
Apr
2
comment Example of where violation of strict positivity condition in inductive types leads to inconsistency
Another reason is that we can add the FAN theorem to Agda, after which we can prove that the type in question is (isomorphic to) natural numbers.
Apr
2
comment Example of where violation of strict positivity condition in inductive types leads to inconsistency
Can we come up with an example which creates an inconsistency all by itself? Your example is inconsistent if we also assume (enough) excluded middle.
Apr
1
revised Why does Coq have Prop?
edited title
Mar
31
awarded  Nice Answer