Search Results
| Search type | Search syntax |
|---|---|
| Tags | [tag] |
| Exact | "words here" |
| Author |
user:1234 user:me (yours) |
| Score |
score:3 (3+) score:0 (none) |
| Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
| Views | views:250 |
| Code | code:"if (foo != bar)" |
| Sections |
title:apples body:"apples oranges" |
| URL | url:"*.example.com" |
| Saves | in:saves |
| Status |
closed:yes duplicate:no migrated:no wiki:no |
| Types |
is:question is:answer |
| Exclude |
-[tag] -apples |
| For more details on advanced search visit our help page | |
Results tagged with reference-request
Search options questions only
not deleted
user 657
Reference-request is used when the author needs to know about work related to the question.
26
votes
1
answer
727
views
Unification and Gaussian Elimination
Does anyone knows of references that precisely spell out the connection between the unification algorithm and Gaussian elimination? I'm particularly interested in the relationship between triangular s …
- 32.9k
9
votes
3
answers
338
views
Resumption-based IO systems?
I've been playing around with resumptions lately, mostly from Abramsky's classic paper Retracing Some Paths in Process Algebra. They are quite slick (basically solutions to the domain equation $R = I …
- 32.9k
22
votes
3
answers
3k
views
Generalizations of Brzozowski's method of derivatives of regular expressions to grammars?
Brzozowski's method of derivatives is a very pretty technique for building deterministic automata from regular expressions in a nicely algebraic way. I've worked out some cute generalizations of this …
- 32.9k
18
votes
1
answer
481
views
Parametricity and projective eliminations for dependent records
It's well-known that in System F, you can encode binary products with the type
$$
A \times B \triangleq \forall\alpha.\; (A \to B \to \alpha) \to \alpha
$$
You can then define projection functions $\p …
- 32.9k
14
votes
0
answers
309
views
Categorical semantics for S5 modal logic?
Does anyone know where I can look to find out what the generally categorical semantics of S5 is?
For S4, the answer is well-known: we want a Cartesian closed category with a product-preserving comon …
- 32.9k
16
votes
2
answers
501
views
Uses of quasi-PERs/difunctional relations/zig-zag relations?
Given sets $A$ and $B$, a difunctional relation $(\sim) \subseteq A \times B$ between them is defined to be a relation satisfying the following property:
If $a \sim b$ and $a' \sim b'$ and $a \sim …
- 32.9k
10
votes
1
answer
329
views
Unification-based elimination rule for equality
A few years back, I ran across the following left-rule for equality in sequent calculus:
$$
\frac{s \doteq t \leadsto \theta \qquad
\theta(\Gamma) \vdash \theta(C)}
{\Gamma, s \doteq t …
- 32.9k
15
votes
1
answer
646
views
Fixed point theorems for constructive metric spaces?
Banach's fixed point theorem says that if we have a nonempty complete metric space $A$, then any uniformly contractive function $f : A \to A$ it has a unique fixed point $\mu(f)$. However, the proof o …
- 32.9k
11
votes
2
answers
350
views
References to programming languages based on conditional logics
Conditional logics are logics which augment traditional logical implication with modal operators corresponding to other notions of condition (for example, the causal conditional $A\; \square\!\!\!\!\t …
- 32.9k
15
votes
2
answers
484
views
Proof theory of biproducts?
A category has biproducts when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts?
Perhaps the best-known example is the cat …
- 32.9k
12
votes
1
answer
323
views
Reference for the fact that (0=1) implies false requires a universe in MLTT
It's a fairly well-known fact that deriving a contradiction from a disequality (for example, $(0=1) \to \bot$) in Martin-Loef type theory requires a universe.
The proof is also fairly straightforwar …
- 32.9k