# Questions tagged [lo.logic]

Computational and mathematical logic.

474 questions
Filter by
Sorted by
Tagged with
361 views

### Original Hoare Logic termination paper

I'm looking for the original paper where Hoare (or someone else I suppose) discusses termination (Total Correctness). Or any other early work on termination for "vanilla" Hoare logic (I suppose by ...
374 views

### MSO properties, planar graphs and minor-free graphs

Courcelle's theorem states that every graph property definable in monadic second-order logic can be decided in linear time on graphs of bounded treewidth. This is one of the most well-known ...
543 views

### Interesting algorithms in the formalization of the Feit-Thompson theorem?

It looks like George Gonthier and his collaborators have finished formalizing the Odd Order Theorem. In his earlier work on the Four Color Theorem, Gonthier invented a bunch of new algorithms (...
119 views

### Formal Methods Applied to Role-Based Security (RBAC)

I wonder if someone could direct me to a basic introduction to formal methods applied to role-based security. I'm particularly interested in the question of formal verification and the kind of ...
321 views

### What can we prove with infinite graphs that we cannot prove without them?

This is a follow-up question to this one about infinite graphs. Answers and comments to that question list objects and situations which are naturally modeled by infinite graphs. But there are also ...
247 views

### Closure ordinals for inductive types with function spaces

Functors built from finite products and sums have closure ordinal $\omega$, detailed nicely in this manuscript by Francois Metayer. i.e. we can reach the inductive type $nat := \mu X. 1 + X$ by ...
1k views

### A mathematical (categorical) description of type classes

A functional language can be viewed as a category where its objects are types and morphisms functions between them. How do type classes fit in this model? I assume we should only consider those ...
250 views

### Problem in embedding

I want to embed PPTL(a kind of logic) in Coq. Because of its complex semantics, I just embed its systax. ...
6k views

### Explaining Applicative functor in categorical terms - monoidal functors

I'd like to understand Applicative in terms of category theory. The documentation for Applicative says that it's a strong lax ...
534 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 ...
342 views

### Encoding a logic in Coq

I want to encode a logic into Coq. The semantics of the logic are very complex and I just want to encode the syntax, axioms, inference rules. I use deep embedding, but I can't use notation like: <...