User Ms. Molly Stewart-Gallus

20 votes

2 answers

3k views

What is bidirectional type checking?

asked Mar 18, 2022 at 23:41

17 votes

2 answers

507 views

What are the advantages to impredicativity?

asked Mar 12, 2022 at 4:50

16 votes

3 answers

1k views

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

asked Apr 30, 2022 at 3:56

13 votes

2 answers

634 views

What is a commuting conversion and why are they problematic?

asked Mar 29, 2022 at 19:07

12 votes

1 answer

507 views

Is induction over mutually inductive coinductive types possible?

asked Mar 5, 2022 at 4:33

12 votes

2 answers

583 views

What is hereditary substitution and why should I use it?

asked Mar 26, 2022 at 20:21

11 votes

1 answer

208 views

Ergonomic use of multicategories in proof assistants

asked Mar 7, 2022 at 3:00

9 votes

1 answer

175 views

How to deal with the proliferation of encodings of ASTs?

asked Mar 30, 2022 at 17:06

9 votes

2 answers

859 views

Construction of inductive types "the hard way"

asked May 10, 2022 at 0:27

9 votes

3 answers

579 views

How to implement a visual proof assistant?

asked Aug 30, 2022 at 18:55

7 votes

0 answers

92 views

What is focusing and how do I use it?

asked May 10, 2022 at 23:51

7 votes

1 answer

230 views

Typing proof trees or proof objects

asked Mar 8, 2022 at 6:23

6 votes

0 answers

115 views

Is every logical theory embeddable in a dependently typed extensional type theory?

asked Mar 16, 2022 at 18:08

6 votes

0 answers

137 views

How to write heavily indexed proofs?

asked Mar 23, 2022 at 19:56

5 votes

1 answer

326 views

What is a weak function space and what does it have to do with HOAS?

asked Jun 7, 2022 at 23:06

5 votes

3 answers

213 views

Mechanization of game semantics?

asked Jun 9, 2022 at 2:39

4 votes

2 answers

277 views

Why do coinductive types require bisimilarity relations?

asked Jun 4, 2022 at 4:50

4 votes

2 answers

452 views

Is there a "standard" encoding or model of material set theory in type theory?

asked Jun 14, 2022 at 16:14

4 votes

2 answers

153 views

Pragmatic encodings of inductive inductive types

asked Oct 17, 2022 at 19:37

4 votes

1 answer

104 views

Use of modal logic in metaprogramming

asked May 25, 2022 at 17:53

3 votes

1 answer

166 views

Is there any work on the use of free logic in proof assistants?

asked May 27, 2022 at 17:26

3 votes

0 answers

79 views

What are some "real world" first order logical theories for demos?

asked May 12, 2022 at 17:01

3 votes

1 answer

158 views

Is there a way to use higher order abstract syntax with linear types?

asked May 20, 2022 at 3:36

3 votes

1 answer

157 views

Partial and multi-valued choice principles/description operators

asked Oct 25, 2022 at 4:40

3 votes

1 answer

115 views

Can you remove strict positivity from mere propositions?

asked Jun 9, 2022 at 2:49

3 votes

1 answer

252 views

Why do record based inductive types with primitive projections lack an eta law?

asked Jun 9, 2022 at 21:43

2 votes

0 answers

55 views

How can I handle side effects within relations?

asked Jun 11, 2022 at 19:28

2 votes

0 answers

73 views

Construction of "free Lawvere theory" on a collection of function symbols

asked Jun 19, 2022 at 22:41

2 votes

1 answer

77 views

How do clausal definitions work?

asked Oct 23, 2022 at 20:52

2 votes

2 answers

198 views

Canonical forms of combinators

asked Sep 7, 2022 at 17:44

Stack Exchange Network

34 Questions

What is bidirectional type checking?

What are the advantages to impredicativity?

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

What is a commuting conversion and why are they problematic?

Is induction over mutually inductive coinductive types possible?

What is hereditary substitution and why should I use it?

Ergonomic use of multicategories in proof assistants

How to deal with the proliferation of encodings of ASTs?

Construction of inductive types "the hard way"

How to implement a visual proof assistant?

What is focusing and how do I use it?

Typing proof trees or proof objects

Is every logical theory embeddable in a dependently typed extensional type theory?

How to write heavily indexed proofs?

What is a weak function space and what does it have to do with HOAS?

Mechanization of game semantics?

Why do coinductive types require bisimilarity relations?

Is there a "standard" encoding or model of material set theory in type theory?

Pragmatic encodings of inductive inductive types

Use of modal logic in metaprogramming

Is there any work on the use of free logic in proof assistants?

What are some "real world" first order logical theories for demos?

Is there a way to use higher order abstract syntax with linear types?

Partial and multi-valued choice principles/description operators

Can you remove strict positivity from mere propositions?

Why do record based inductive types with primitive projections lack an eta law?

How can I handle side effects within relations?

Construction of "free Lawvere theory" on a collection of function symbols

How do clausal definitions work?

Canonical forms of combinators