Found 32 Documents (Results 1–32)
A reduction-preserving completion for proving confluence of non-terminating term rewriting systems. (English) Zbl 1238.68071
MSC:
68Q42
A synthesis of the procedural and declarative styles of interactive theorem proving. (English) Zbl 1238.68147
MSC:
68T15
03B35
Preservation of strong normalisation modulo permutations for the structural \(\lambda\)-calculus. (English) Zbl 1237.03011
Static analysis of run-time errors in embedded real-time parallel C programs. (English) Zbl 1238.68048
MSC:
68N19
Theorem proving for prenex Gödel logic with \(\Delta\): checking validity and unsatisfiability. (English) Zbl 1238.03021
Derivation lengths classification of Gödel’s T extending Howard’s assignment. (English) Zbl 1238.03025
A bi-directional refinement algorithm for the calculus of (co)inductive constructions. (English) Zbl 1238.68145
MSC:
68T15
Typing copyless message passing. (English) Zbl 1238.68095
MSC:
68Q85
Type-elimination-based reasoning for the description logic \(\mathcal {SHIQ}b_s\) using decision diagrams and disjunctive Datalog. (English) Zbl 1241.68109
Absorbing subalgebras, cyclic terms, and the constraint satisfaction problem. (English) Zbl 1239.08002
On completeness of reducibility candidates as a semantics of strong normalization. (English) Zbl 1239.03033
MSC:
03F05
Filter Results by …
all
top 5
Author
- Padovani, Luca (2)
- Abel, Andreas M. (1)
- Accattoli, Beniamino (1)
- Adjé, Assalé (1)
- Adler, Isolde (1)
- Aoto, Takahito (1)
- Arrighi, Pablo (1)
- Asperti, Andrea (1)
- Baaz, Matthias (1)
- Barto, Libor (1)
- Bojańczyk, Mikołaj (1)
- Bono, Viviana (1)
- Braibant, Thomas (1)
- Castagna, Giuseppe (1)
- Chen, Feng (1)
- Cheney, James (1)
- Ciabattoni, Agata (1)
- Cohen, Cyril (1)
- Cook, Stephen Arthur (1)
- Cousineau, Denis (1)
- Dezani-Ciancaglini, Mariangiola (1)
- Díaz-Caro, Alejandro (1)
- Fermüller, Christian G. (1)
- Figueira, Diego (1)
- Fogarty, Seth J. (1)
- Fontes, Lila (1)
- Fuchs, Alexander (1)
- Gaubert, Stéphane (1)
- Goel, Amit (1)
- Goubault-Larrecq, Jean (1)
- Goubault, Eric (1)
- Grundy, Jim (1)
- Halpern, Joseph Yehuda (1)
- Hitzler, Pascal (1)
- Kesner, Delia (1)
- Kozik, Marcin (1)
- Kreutzer, Stephan (1)
- Krivine, Jean-Louis (1)
- Krötzsch, Markus (1)
- Krstic, Sava A. (1)
- Lasota, Sławomir (1)
- Lowe, Gavin (1)
- Mahboubi, Assia (1)
- Mazur, Tomasz (1)
- Miné, Antoine (1)
- Potgieter, Paul (1)
- Pous, Damien (1)
- Pucella, Riccardo (1)
- Ricciotti, Wilmer (1)
- Roşu, Grigore (1)
- Rudolph, Sebastian (1)
- Sacerdoti Coen, Claudio (1)
- Scherer, Gabriel (1)
- Schwentick, Thomas (1)
- Tassi, Enrico (1)
- Tinelli, Cesare (1)
- Toyama, Yoshihito (1)
- Vardi, Moshe Ya’akov (1)
- Weiermann, Andreas (1)
- Weyer, Mark (1)
- Wiedijk, Freek (1)
- Wilken, Gunnar (1)
- Zeume, Thomas (1)
all
top 3
Software
- Coq (7)
- Agda (3)
- Automath (3)
- Casper (2)
- XPath (2)
- ASTREE (1)
- AspectJ (1)
- Cayenne (1)
- Clara (1)
- CoLoR (1)
- Coq/SSReflect (1)
- CoqMT (1)
- DPT (1)
- DaCapo (1)
- FOCI (1)
- Freshml (1)
- HOL (1)
- HOL Light (1)
- Isabelle/Isar (1)
- Isar (1)
- J-LO (1)
- Java-MOP (1)
- Lurupa (1)
- Matita (1)
- Metamath (1)
- Mizar (1)
- MizarMode (1)
- PVS (1)
- PhoX (1)
- Proof General (1)
- QEPCAD (1)
- RALL (1)
- Regular Sets (1)
- SIMPLIFY (1)
- SMT-LIB (1)
- SeDuMi (1)
- Theorema (1)
- Twelf (1)
- YALMIP (1)
- dedukti (1)
- miz3 (1)
- seL4 (1)