# Questions tagged [formal-systems]

The tag has no usage guidance.

8 questions
84 views

### Representable functions on System T

In Proof and Types by Girard et alii. Section 7.4.2, I think that the authors want to show that: (1) The set of functions definable in System T coincides with the set of recursive functions whose ...
123 views

### System F and System T names

Does anyone know where do the names System "F" and System "T" comes from? I am not asking who introduced those names (Girard System F, and Gödel System T), but what the "F" and the "T" means.
47 views

### semantics of “destroy object” in HRU model

In the access control model HRU there is the primitive request destroy object o which is only defined if o is an object in the current protection state which is not a subject. I am interested in why ...
84 views

### Salomaa's axiomatisation of regular languages and the use of regular expression in it

I am reading the classical article of A. Salomaa where he gives two axiom systems for regular sets and proofs consistency and completeness. As I have understood it, an axiomatic system in some logic (...
361 views

### Derivation of cut rule in sequent calculus

I searched internet but could not find any good weblink which shows how the cut rule for sequent calculus can be derived. I found this paper but it uses implication elimination rule which I cannot ...
1k views

### How can we know that formal methods work?

An important goal of formal methods is to prove the correctness of systems, either by automated or human-directed means. However, it seems that even if you can give a correctness proof, you may NOT be ...
760 views

### Formal Semantics of Programming Languages

I'm new to programming languages theory and I'm seeking for a good resource on a resource for formal semantics of programming languages. Specifically looking for structural operational semantics. I ...
439 views

### Books on Mu-Calculus

I need a book on Mu-Calculus with lots of examples that can be used for self-study and preparation for exams.