User Molossus Spondee - Proof Assistants Stack Exchange

Molossus Spondee

Member for 1 year, 1 month
Last seen this week

gitlab.com/mstewartgallus
Vancouver

Stats

2,628

reputation

15k

reached

23

answers

34

questions

Loading…

Communities

About

I have an amateur interest in type theory , maths and pictures of cute animals.

Badges

View all badges

This user doesn’t have any gold badges yet.

5

silver badges

Inquisitive

Oct 29
Enthusiast

Apr 3, 2022
Beta

Mar 15, 2022

20

bronze badges

Popular Question

Aug 9
Curious

Mar 17, 2022
Commentator

Mar 12, 2022

Top tags

type-theory

8

Score

13

Posts

23

Posts %

category-theory

7

Score

5

Posts

9

Posts %

coq

6

Score

11

Posts

19

Posts %

inductive-type

3

Score

7

Posts

12

Posts %

design

2

Score

3

Posts

5

Posts %

foundations

1

Score

4

Posts

7

Posts %

Top posts

View all questions and answers

All Questions Answers

Score Newest

17

What are the advantages to impredicativity?

Mar 12, 2022

16

What is bidirectional type checking?

Mar 18, 2022

15

Do you need a Hilbert style Epsilon operator for definitions in set theory?

Apr 30, 2022

13

What is a commuting conversion and why are they problematic?

Mar 29, 2022

12

Is induction over mutually inductive coinductive types possible?

Mar 5, 2022

11

Ergonomic use of multicategories in proof assistants

Mar 7, 2022

9

Construction of inductive types "the hard way"

May 10, 2022

8

How to deal with the proliferation of encodings of ASTs?

Mar 30, 2022

8

What is hereditary substitution and why should I use it?

Mar 26, 2022

7

How to implement a visual proof assistant?

Aug 30, 2022

Top network posts

View all network posts

27

How can I make my stack monad faster?

18

Why doesn't matter clump together such that it can't be taken apart again?

18

Is Pauli-repulsion a "force" that is completely separate from the 4 fundamental forces?

17

How can I get JHC to cooperate with the android ndk?

17

What is the shape of a deuterium nucleus?