Area 51 » Andrej Bauer

info activity reputation

2,625

reputation

359 views

discussion user

network profile

Registered User

name	Andrej Bauer
member for	9 years
seen	Dec 15 '22 at 7:54
website	andrej.com
location	Ljubljana

I am a professional mathematician. My area of research is logic, constructive and computable mathematics, category theory, and semantics of programming languages.

stats accounts

Proposal

670

days

Proof Assistants

For mathematicians and computer scientists who develop and use proof assistants.

define

commit

public beta

Current Commitments

Fulfilled Commitment

670

days

Proof Assistants

For mathematicians and computer scientists who develop and use proof assistants.

define

commit

public beta

Followed

Example Questions

votes newest recent

Proof Assistants: I am a long-time Coq user who is learning Lean. Is there a short translation table mapping Coq tactics to corresponding Lean tactics?

Proof Assistants: What is a better way of doing this in Lean: `have H := …, simp at H, apply H`? If I just do `apply …` it fails to match against the goal.

Proof Assistants: Agda often inserts fully qualified names on `C-c C-c`, e.g., `Some.Module.foo` instead of `foo`, where `Some.Module` is opened. Is there a fix?

Proof Assistants: How do I create a list of graphs in Lean? All elements of a list must share the same type, but graphs depend on their vertex types.

Proof Assistants: Can I connect a proof assistant with a computer algebra system such as Mathematica or Maple?

Programming Language Design and Implementation: What compilation techniques for algebraic effects and handlers are known that focus on producing practical efficient code?

Votes Cast

10 up

0 down

Badges

● Nice Question × 6
● Upholder
● Activist
● Campaigner

● Promoter
● Lobbyist
● Revolution
● Movement

● Mortarboard
● Grassroots
● Centrist
● Advocate

● Filibuster
● Pioneer
● Caucus
● Autobiographer

user feed