Ehrhard, Thomas A coherent differential PCF. (English) Zbl 07788979 Log. Methods Comput. Sci. 19, No. 4, Paper No. 7, 88 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{T. Ehrhard}, Log. Methods Comput. Sci. 19, No. 4, Paper No. 7, 88 p. (2023; Zbl 07788979) Full Text: DOI arXiv
Grabmayer, Clemens A coinductive reformulation of Milner’s proof system for regular expressions modulo bisimilarity. (English) Zbl 07731928 Log. Methods Comput. Sci. 19, No. 2, Paper No. 17, 57 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{C. Grabmayer}, Log. Methods Comput. Sci. 19, No. 2, Paper No. 17, 57 p. (2023; Zbl 07731928) Full Text: DOI arXiv
van den Berg, Benno; Passmann, Robert Converse extensionality and apartness. (English) Zbl 07639909 Log. Methods Comput. Sci. 18, No. 4, Paper No. 13, 21 p. (2022). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{B. van den Berg} and \textit{R. Passmann}, Log. Methods Comput. Sci. 18, No. 4, Paper No. 13, 21 p. (2022; Zbl 07639909) Full Text: DOI arXiv
Acclavio, Matteo; Horne, Ross; Straßburger, Lutz An analytic propositional proof system on graphs. (English) Zbl 07639905 Log. Methods Comput. Sci. 18, No. 4, Paper No. 1, 80 p. (2022). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{M. Acclavio} et al., Log. Methods Comput. Sci. 18, No. 4, Paper No. 1, 80 p. (2022; Zbl 07639905) Full Text: DOI arXiv
Ehrhard, Thomas Differentials and distances in probabilistic coherence spaces. (English) Zbl 1528.68064 Log. Methods Comput. Sci. 18, No. 3, Paper No. 2, 33 p. (2022). MSC: 68N18 03F52 68Q55 PDFBibTeX XMLCite \textit{T. Ehrhard}, Log. Methods Comput. Sci. 18, No. 3, Paper No. 2, 33 p. (2022; Zbl 1528.68064) Full Text: arXiv Link
Sterling, Jonathan; Angiuli, Carlo; Gratzer, Daniel A cubical language for Bishop sets. (English) Zbl 07566056 Log. Methods Comput. Sci. 18, No. 1, Paper No. 43, 80 p. (2022). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{J. Sterling} et al., Log. Methods Comput. Sci. 18, No. 1, Paper No. 43, 80 p. (2022; Zbl 07566056) Full Text: arXiv Link
Bauer, Andrej; Petković Komel, Anja An extensible equality checking algorithm for dependent type theories. (English) Zbl 1504.68276 Log. Methods Comput. Sci. 18, No. 1, Paper No. 17, 42 p. (2022). MSC: 68V15 03B38 PDFBibTeX XMLCite \textit{A. Bauer} and \textit{A. Petković Komel}, Log. Methods Comput. Sci. 18, No. 1, Paper No. 17, 42 p. (2022; Zbl 1504.68276) Full Text: arXiv Link
Hernest, Dan; Trifonov, Trifon Modal functional (“Dialectica”) interpretation. (English) Zbl 07471663 Log. Methods Comput. Sci. 17, No. 4, Paper No. 3, 29 p. (2021). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{D. Hernest} and \textit{T. Trifonov}, Log. Methods Comput. Sci. 17, No. 4, Paper No. 3, 29 p. (2021; Zbl 07471663) Full Text: arXiv Link
Mahboubi, Assia; Sibut-Pinote, Thomas A formal proof of the irrationality of \(\zeta(3)\). (English) Zbl 1509.68311 Log. Methods Comput. Sci. 17, No. 1, Paper No. 16, 25 p. (2021). MSC: 68V15 11J72 11M06 68W30 PDFBibTeX XMLCite \textit{A. Mahboubi} and \textit{T. Sibut-Pinote}, Log. Methods Comput. Sci. 17, No. 1, Paper No. 16, 25 p. (2021; Zbl 1509.68311) Full Text: arXiv Link
Xu, Chuangjie A syntactic approach to continuity of T-definable functionals. (English) Zbl 1528.03115 Log. Methods Comput. Sci. 16, No. 1, Paper No. 22, 11 p. (2020). MSC: 03B38 03B40 03F10 03F65 PDFBibTeX XMLCite \textit{C. Xu}, Log. Methods Comput. Sci. 16, No. 1, Paper No. 22, 11 p. (2020; Zbl 1528.03115) Full Text: arXiv Link
Das, Anupam On the logical complexity of cyclic arithmetic. (English) Zbl 1528.03240 Log. Methods Comput. Sci. 16, No. 1, Paper No. 1, 39 p. (2020). MSC: 03F30 03F20 PDFBibTeX XMLCite \textit{A. Das}, Log. Methods Comput. Sci. 16, No. 1, Paper No. 1, 39 p. (2020; Zbl 1528.03240) Full Text: arXiv
Seiller, Thomas Interaction graphs: exponentials. (English) Zbl 1509.03168 Log. Methods Comput. Sci. 15, No. 3, Paper No. 25, 58 p. (2019). MSC: 03F52 68Q55 PDFBibTeX XMLCite \textit{T. Seiller}, Log. Methods Comput. Sci. 15, No. 3, Paper No. 25, 58 p. (2019; Zbl 1509.03168) Full Text: arXiv
Demirci, Gökalp; Hirvensalo, Mika; Reinhardt, Klaus; Say, A. C. Cem; Yakaryılmaz, Abuzer Alternating, private alternating, and quantum alternating realtime automata. (English) Zbl 1509.68067 Log. Methods Comput. Sci. 15, No. 3, Paper No. 22, 21 p. (2019). MSC: 68Q04 68Q12 81P68 PDFBibTeX XMLCite \textit{G. Demirci} et al., Log. Methods Comput. Sci. 15, No. 3, Paper No. 22, 21 p. (2019; Zbl 1509.68067) Full Text: arXiv
Berardi, Stefano; Tatsuta, Makoto Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proofs. (English) Zbl 1509.03158 Log. Methods Comput. Sci. 15, No. 3, Paper No. 10, 25 p. (2019). MSC: 03F07 03D70 PDFBibTeX XMLCite \textit{S. Berardi} and \textit{M. Tatsuta}, Log. Methods Comput. Sci. 15, No. 3, Paper No. 10, 25 p. (2019; Zbl 1509.03158) Full Text: arXiv
Engeler, Erwin A forgotten theory of proofs? (English) Zbl 1509.03157 Log. Methods Comput. Sci. 15, No. 3, Paper No. 6, 6 p. (2019). MSC: 03F03 PDFBibTeX XMLCite \textit{E. Engeler}, Log. Methods Comput. Sci. 15, No. 3, Paper No. 6, 6 p. (2019; Zbl 1509.03157) Full Text: arXiv
Dagnino, Francesco Coaxioms: flexible coinductive definitions by inference systems. (English) Zbl 1432.68251 Log. Methods Comput. Sci. 15, No. 1, Paper No. 26, 48 p. (2019). MSC: 68Q55 03B35 03B70 03F07 06B23 PDFBibTeX XMLCite \textit{F. Dagnino}, Log. Methods Comput. Sci. 15, No. 1, Paper No. 26, 48 p. (2019; Zbl 1432.68251) Full Text: arXiv
Ahrens, Benedikt; Lefanu Lumsdaine, Peter Displayed categories. (English) Zbl 1419.18001 Log. Methods Comput. Sci. 15, No. 1, Paper No. 20, 18 p. (2019). Reviewer: Marco Benini (Buccinasco) MSC: 18A15 03B15 PDFBibTeX XMLCite \textit{B. Ahrens} and \textit{P. Lefanu Lumsdaine}, Log. Methods Comput. Sci. 15, No. 1, Paper No. 20, 18 p. (2019; Zbl 1419.18001) Full Text: arXiv
Zeilberger, Noam A sequent calculus for a semi-associative law. (English) Zbl 1515.03223 Log. Methods Comput. Sci. 15, No. 1, Paper No. 9, 23 p. (2019). MSC: 03F52 03F05 03B40 06A07 PDFBibTeX XMLCite \textit{N. Zeilberger}, Log. Methods Comput. Sci. 15, No. 1, Paper No. 9, 23 p. (2019; Zbl 1515.03223) Full Text: arXiv
Grädel, Erich; Grohe, Martin; Pago, Benedikt; Pakusa, Wied A finite-model-theoretic view on propositional proof complexity. (English) Zbl 1451.03023 Log. Methods Comput. Sci. 15, No. 1, Paper No. 4, 53 p. (2019). MSC: 03C13 03F20 68Q19 PDFBibTeX XMLCite \textit{E. Grädel} et al., Log. Methods Comput. Sci. 15, No. 1, Paper No. 4, 53 p. (2019; Zbl 1451.03023) Full Text: arXiv
Ramanayake, Revantha Inducing syntactic cut-elimination for indexed nested sequents. (English) Zbl 1528.03235 Log. Methods Comput. Sci. 14, No. 4, Paper No. 18, 25 p. (2018). MSC: 03F05 03B45 PDFBibTeX XMLCite \textit{R. Ramanayake}, Log. Methods Comput. Sci. 14, No. 4, Paper No. 18, 25 p. (2018; Zbl 1528.03235) Full Text: DOI arXiv
Docherty, Simon; Pym, David Intuitionistic layered graph logic: semantics and proof theory. (English) Zbl 1454.03030 Log. Methods Comput. Sci. 14, No. 4, Paper No. 11, 36 p. (2018). MSC: 03B47 03B20 03F03 PDFBibTeX XMLCite \textit{S. Docherty} and \textit{D. Pym}, Log. Methods Comput. Sci. 14, No. 4, Paper No. 11, 36 p. (2018; Zbl 1454.03030) Full Text: DOI arXiv
Rinaldi, Davide; Wessel, Daniel Extension by conservation. Sikorski’s theorem. (English) Zbl 1454.03085 Log. Methods Comput. Sci. 14, No. 4, Paper No. 8, 17 p. (2018). MSC: 03F60 03F03 06D05 06E05 PDFBibTeX XMLCite \textit{D. Rinaldi} and \textit{D. Wessel}, Log. Methods Comput. Sci. 14, No. 4, Paper No. 8, 17 p. (2018; Zbl 1454.03085) Full Text: DOI arXiv
Aubert, Clément; Bagnol, Marc Unification and logarithmic space. (English) Zbl 1447.68005 Log. Methods Comput. Sci. 14, No. 3, Paper No. 6, 21 p. (2018). Reviewer: Guillermo Morales Luna (Ciudad de México) MSC: 68Q15 03F52 68N17 68Q42 68Q45 PDFBibTeX XMLCite \textit{C. Aubert} and \textit{M. Bagnol}, Log. Methods Comput. Sci. 14, No. 3, Paper No. 6, 21 p. (2018; Zbl 1447.68005) Full Text: DOI arXiv
Litak, Tadeusz; Pattinson, Dirk; Sano, Katsuhiko; Schröder, Lutz Model theory and proof theory of coalgebraic predicate logic. (English) Zbl 1459.03104 Log. Methods Comput. Sci. 14, No. 1, Paper No. 22, 52 p. (2018). MSC: 03G30 03B45 03C50 03F03 03F05 PDFBibTeX XMLCite \textit{T. Litak} et al., Log. Methods Comput. Sci. 14, No. 1, Paper No. 22, 52 p. (2018; Zbl 1459.03104) Full Text: DOI arXiv
Diaconescu, Denisa; Metcalfe, George; Schnüriger, Laura A real-valued modal logic. (English) Zbl 1459.03021 Log. Methods Comput. Sci. 14, No. 1, Paper No. 10, 27 p. (2018). MSC: 03B45 03B50 03D15 03F05 PDFBibTeX XMLCite \textit{D. Diaconescu} et al., Log. Methods Comput. Sci. 14, No. 1, Paper No. 10, 27 p. (2018; Zbl 1459.03021) Full Text: DOI arXiv
Hetzl, Stefan; Wong, Tin Lok Some observations on the logical foundations of inductive theorem proving. (English) Zbl 1460.03005 Log. Methods Comput. Sci. 13, No. 4, Paper No. 10, 26 p. (2017). MSC: 03B35 03C62 03F05 PDFBibTeX XMLCite \textit{S. Hetzl} and \textit{T. L. Wong}, Log. Methods Comput. Sci. 13, No. 4, Paper No. 10, 26 p. (2017; Zbl 1460.03005) Full Text: DOI arXiv
Hansen, Helle Hvid; Kupke, Clemens; Rutten, Jan Stream differential equations: specification formats and solution methods. (English) Zbl 1451.68181 Log. Methods Comput. Sci. 13, No. 1, Paper No. 3, 51 p. (2017). MSC: 68Q70 68Q10 68Q42 PDFBibTeX XMLCite \textit{H. H. Hansen} et al., Log. Methods Comput. Sci. 13, No. 1, Paper No. 3, 51 p. (2017; Zbl 1451.68181) Full Text: DOI arXiv
Das, Anupam; Straßburger, Lutz On linear rewriting systems for Boolean logic and some applications to proof theory. (English) Zbl 1445.03069 Log. Methods Comput. Sci. 12, No. 4, Paper No. 9, 27 p. (2016). MSC: 03F52 03F20 03B05 68Q42 68Q17 PDFBibTeX XMLCite \textit{A. Das} and \textit{L. Straßburger}, Log. Methods Comput. Sci. 12, No. 4, Paper No. 9, 27 p. (2016; Zbl 1445.03069) Full Text: DOI arXiv
Bruscoli, Paola; Guglielmi, Alessio; Gundersen, Tom; Parigot, Michel Quasipolynomial normalisation in deep inference via atomic flows and threshold formulae. (English) Zbl 1448.03045 Log. Methods Comput. Sci. 12, No. 2, Paper No. 5, 30 p. (2016). MSC: 03F05 03F20 PDFBibTeX XMLCite \textit{P. Bruscoli} et al., Log. Methods Comput. Sci. 12, No. 2, Paper No. 5, 30 p. (2016; Zbl 1448.03045) Full Text: DOI
Kerjean, Marie Weak topologies for linear logic. (English) Zbl 1448.03014 Log. Methods Comput. Sci. 12, No. 1, Paper No. 3, 23 p. (2016). MSC: 03B47 03F52 46A20 68Q55 PDFBibTeX XMLCite \textit{M. Kerjean}, Log. Methods Comput. Sci. 12, No. 1, Paper No. 3, 23 p. (2016; Zbl 1448.03014) Full Text: DOI arXiv
Neumann, Eike Computational problems in metric fixed point theory and their Weihrauch degrees. (English) Zbl 1351.03054 Log. Methods Comput. Sci. 11, No. 4, Paper No. 20, 44 p. (2015). MSC: 03F10 03F60 03D30 03D15 47H10 PDFBibTeX XMLCite \textit{E. Neumann}, Log. Methods Comput. Sci. 11, No. 4, Paper No. 20, 44 p. (2015; Zbl 1351.03054) Full Text: DOI arXiv
Bauer, Matthew Steven The computational complexity of propositional cirquent calculus. (English) Zbl 1328.03043 Log. Methods Comput. Sci. 11, No. 1, Paper No. 12, 16 p. (2015). MSC: 03D15 03B47 03F07 PDFBibTeX XMLCite \textit{M. S. Bauer}, Log. Methods Comput. Sci. 11, No. 1, Paper No. 12, 16 p. (2015; Zbl 1328.03043) Full Text: DOI arXiv
Das, Anupam On the relative proof complexity of deep inference via atomic flows. (English) Zbl 1358.03089 Log. Methods Comput. Sci. 11, No. 1, Paper No. 4, 23 p. (2015). MSC: 03F20 PDFBibTeX XMLCite \textit{A. Das}, Log. Methods Comput. Sci. 11, No. 1, Paper No. 4, 23 p. (2015; Zbl 1358.03089) Full Text: DOI arXiv
Bellin, Gianluigi Categorical proof theory of co-intuitionistic linear logic. (English) Zbl 1341.03092 Log. Methods Comput. Sci. 10, No. 3, Paper No. 16, 36 p. (2014). MSC: 03F52 03B70 03G30 68Q55 PDFBibTeX XMLCite \textit{G. Bellin}, Log. Methods Comput. Sci. 10, No. 3, Paper No. 16, 36 p. (2014; Zbl 1341.03092) Full Text: DOI arXiv
Kahramanoğullari, Ozan Interaction and depth against nondeterminism in proof search. (English) Zbl 1433.03147 Log. Methods Comput. Sci. 10, No. 2, Paper No. 5, 49 p. (2014). MSC: 03F52 03F20 PDFBibTeX XMLCite \textit{O. Kahramanoğullari}, Log. Methods Comput. Sci. 10, No. 2, Paper No. 5, 49 p. (2014; Zbl 1433.03147) Full Text: DOI arXiv
Møgelberg, Rasmus Ejlers; Staton, Sam Linear usage of state. (English) Zbl 1326.68070 Log. Methods Comput. Sci. 10, No. 1, Paper No. 17, 52 p. (2014). MSC: 68N18 03F52 18C15 18C50 PDFBibTeX XMLCite \textit{R. E. Møgelberg} and \textit{S. Staton}, Log. Methods Comput. Sci. 10, No. 1, Paper No. 17, 52 p. (2014; Zbl 1326.68070) Full Text: DOI arXiv
Berardi, Stefano; De’Liguoro, Ugo Knowledge spaces and the completeness of learning strategies. (English) Zbl 1326.68167 Log. Methods Comput. Sci. 10, No. 1, Paper No. 9, 23 p. (2014). MSC: 68Q32 03F10 PDFBibTeX XMLCite \textit{S. Berardi} and \textit{U. De'Liguoro}, Log. Methods Comput. Sci. 10, No. 1, Paper No. 9, 23 p. (2014; Zbl 1326.68167) Full Text: DOI arXiv
Hetzl, Stefan; Straßburger, Lutz Herbrand-confluence. (English) Zbl 1325.03069 Log. Methods Comput. Sci. 9, No. 4, Paper No. 26, 25 p. (2013). Reviewer: Andrzej Indrzejczak (Łódź) MSC: 03F05 PDFBibTeX XMLCite \textit{S. Hetzl} and \textit{L. Straßburger}, Log. Methods Comput. Sci. 9, No. 4, Paper No. 26, 25 p. (2013; Zbl 1325.03069) Full Text: DOI arXiv
Müller, Sebastian Polylogarithmic cuts in models of \(\mathbf{V}^{0}\). (English) Zbl 1280.03056 Log. Methods Comput. Sci. 9, No. 1, Paper No. 17, 16 p. (2013). Reviewer: Leszek Aleksander Kołodziejczyk (Warszawa) MSC: 03F20 03C62 03F30 03H15 PDFBibTeX XMLCite \textit{S. Müller}, Log. Methods Comput. Sci. 9, No. 1, Paper No. 17, 16 p. (2013; Zbl 1280.03056) Full Text: DOI arXiv
Platzer, André A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems. (English) Zbl 1261.03113 Log. Methods Comput. Sci. 8, No. 4, Paper No. 17, 44 p. (2012). MSC: 03B70 34A38 68M14 68Q60 PDFBibTeX XMLCite \textit{A. Platzer}, Log. Methods Comput. Sci. 8, No. 4, Paper No. 17, 44 p. (2012; Zbl 1261.03113) Full Text: DOI arXiv
Platzer, André The structure of differential invariants and differential cut elimination. (English) Zbl 1261.03112 Log. Methods Comput. Sci. 8, No. 4, Paper No. 16, 38 p. (2012). MSC: 03B70 03F05 34A38 34C14 68Q60 PDFBibTeX XMLCite \textit{A. Platzer}, Log. Methods Comput. Sci. 8, No. 4, Paper No. 16, 38 p. (2012; Zbl 1261.03112) Full Text: DOI arXiv
Braibant, Thomas; Pous, Damien Deciding Kleene algebras in Coq. (English) Zbl 1238.68146 Log. Methods Comput. Sci. 8, No. 1, Paper No. 16, 42 p. (2012). MSC: 68T15 68Q45 68Q70 PDFBibTeX XMLCite \textit{T. Braibant} and \textit{D. Pous}, Log. Methods Comput. Sci. 8, No. 1, Paper No. 16, 42 p. (2012; Zbl 1238.68146) Full Text: DOI
Arrighi, Pablo; Díaz-Caro, Alejandro A System F accounting for scalars. (English) Zbl 1239.03008 Log. Methods Comput. Sci. 8, No. 1, Paper No. 11, 32 p. (2012). MSC: 03B40 03F52 PDFBibTeX XMLCite \textit{P. Arrighi} and \textit{A. Díaz-Caro}, Log. Methods Comput. Sci. 8, No. 1, Paper No. 11, 32 p. (2012; Zbl 1239.03008) Full Text: DOI
Lee, Gyesik; Werner, Benjamin Proof-irrelevant model of CC with predicative induction and judgmental equality. (English) Zbl 1237.03008 Log. Methods Comput. Sci. 7, No. 4, Paper No. 5, 25 p. (2011). MSC: 03B15 03B35 03B40 03E30 PDFBibTeX XMLCite \textit{G. Lee} and \textit{B. Werner}, Log. Methods Comput. Sci. 7, No. 4, Paper No. 5, 25 p. (2011; Zbl 1237.03008) Full Text: DOI arXiv
Metcalfe, George; Olivetti, Nicola Towards a proof theory of Gödel modal logics. (English) Zbl 1266.03044 Log. Methods Comput. Sci. 7, No. 2, Paper No. 10, 27 p. (2011). MSC: 03B52 03B45 PDFBibTeX XMLCite \textit{G. Metcalfe} and \textit{N. Olivetti}, Log. Methods Comput. Sci. 7, No. 2, Paper No. 10, 27 p. (2011; Zbl 1266.03044) Full Text: DOI arXiv
Abel, Andreas; Coquand, Thierry; Pagano, Miguel A modular type-checking algorithm for type theory with singleton types and proof irrelevance. (English) Zbl 1213.68199 Log. Methods Comput. Sci. 7, No. 2, Paper No. 4, 57 p. (2011). MSC: 68N30 03B70 PDFBibTeX XMLCite \textit{A. Abel} et al., Log. Methods Comput. Sci. 7, No. 2, Paper No. 4, 57 p. (2011; Zbl 1213.68199) Full Text: DOI
Miquel, Alexandre Existential witness extraction in classical realizability and via a negative translation. (English) Zbl 1218.03016 Log. Methods Comput. Sci. 7, No. 2, Paper No. 2, 47 p. (2011). MSC: 03B40 03F35 68N30 PDFBibTeX XMLCite \textit{A. Miquel}, Log. Methods Comput. Sci. 7, No. 2, Paper No. 2, 47 p. (2011; Zbl 1218.03016) Full Text: DOI
Ferreira, Gilda; Oliva, Paulo Functional interpretations of intuitionistic linear logic. (English) Zbl 1227.03079 Log. Methods Comput. Sci. 7, No. 1, Paper No. 9, 22 p. (2011). Reviewer: G. E. Mints (Stanford) MSC: 03F52 03F10 03F55 PDFBibTeX XMLCite \textit{G. Ferreira} and \textit{P. Oliva}, Log. Methods Comput. Sci. 7, No. 1, Paper No. 9, 22 p. (2011; Zbl 1227.03079) Full Text: DOI
Berger, Ulrich From coinductive proofs to exact real arithmetic: theory and applications. (English) Zbl 1218.03036 Log. Methods Comput. Sci. 7, No. 1, Paper No. 8, 24 p. (2011). MSC: 03F60 03D78 68N30 PDFBibTeX XMLCite \textit{U. Berger}, Log. Methods Comput. Sci. 7, No. 1, Paper No. 8, 24 p. (2011; Zbl 1218.03036) Full Text: DOI
Lengrand, Stéphane Jean Eric; Dyckhoff, Roy; McKinna, James A focused sequent calculus framework for proof search in pure type systems. (English) Zbl 1218.03010 Log. Methods Comput. Sci. 7, No. 1, Paper No. 6, 35 p. (2011). MSC: 03B35 03F05 03F07 PDFBibTeX XMLCite \textit{S. J. E. Lengrand} et al., Log. Methods Comput. Sci. 7, No. 1, Paper No. 6, 35 p. (2011; Zbl 1218.03010) Full Text: DOI arXiv
Pattinson, Dirk; Schröder, Lutz Generic modal cut elimination applied to conditional logics. (English) Zbl 1232.03049 Log. Methods Comput. Sci. 7, No. 1, Paper No. 4, 28 p. (2011). Reviewer: G. E. Mints (Stanford) MSC: 03F05 03B45 03B47 03F52 PDFBibTeX XMLCite \textit{D. Pattinson} and \textit{L. Schröder}, Log. Methods Comput. Sci. 7, No. 1, Paper No. 4, 28 p. (2011; Zbl 1232.03049) Full Text: DOI
Burel, Guillaume Efficiently simulating higher-order arithmetic by a first-order theory modulo. (English) Zbl 1218.03007 Log. Methods Comput. Sci. 7, No. 1, Paper No. 3, 31 p. (2011). MSC: 03B35 03B15 03F20 03F35 68Q42 PDFBibTeX XMLCite \textit{G. Burel}, Log. Methods Comput. Sci. 7, No. 1, Paper No. 3, 31 p. (2011; Zbl 1218.03007) Full Text: DOI
Aschieri, Federico; Berardi, Stefano Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\). (English) Zbl 1201.03052 Log. Methods Comput. Sci. 6, No. 3, Paper No. 19, 22 p. (2010). MSC: 03F30 03F25 PDFBibTeX XMLCite \textit{F. Aschieri} and \textit{S. Berardi}, Log. Methods Comput. Sci. 6, No. 3, Paper No. 19, 22 p. (2010; Zbl 1201.03052) Full Text: DOI arXiv
Droste, Manfred; Zhang, Guo-Qiang Bifinite Chu spaces. (English) Zbl 1189.68073 Log. Methods Comput. Sci. 6, No. 1, Paper No. 3, 20 p. (2010). MSC: 68Q55 03F52 03G30 18A35 PDFBibTeX XMLCite \textit{M. Droste} and \textit{G.-Q. Zhang}, Log. Methods Comput. Sci. 6, No. 1, Paper No. 3, 20 p. (2010; Zbl 1189.68073) Full Text: DOI
Benzmüller, Christoph E.; Brown, Chad E.; Kohlhase, Michael Cut-simulation and impredicativity. (English) Zbl 1160.03004 Log. Methods Comput. Sci. 5, No. 1, Paper 8, 21 p. (2009). MSC: 03B35 03B15 03F05 PDFBibTeX XMLCite \textit{C. E. Benzmüller} et al., Log. Methods Comput. Sci. 5, No. 1, Paper 8, 21 p. (2009; Zbl 1160.03004) Full Text: DOI arXiv
Werner, Benjamin On the strength of proof-irrelevant type theories. (English) Zbl 1151.03317 Log. Methods Comput. Sci. 4, No. 3, Paper 13, 20 p. (2008). MSC: 03B15 03B35 03B70 68T15 PDFBibTeX XMLCite \textit{B. Werner}, Log. Methods Comput. Sci. 4, No. 3, Paper 13, 20 p. (2008; Zbl 1151.03317) Full Text: DOI