Revisiting the correspondence between cut elimination and normalisation. Zbl 0973.03073
Espírito Santo, José |
|
2000
|
Delayed substitutions. Zbl 1203.68031
Espírito Santo, José |
|
2007
|
Completing Herbelin’s programme. Zbl 1215.03023
Espírito Santo, José |
|
2007
|
Permutative conversions in intuitionistic multiary sequent calculi with cuts. Zbl 1041.03040
Espírito Santo, José; Pinto, Luís |
|
2003
|
Characterising strongly normalising intuitionistic terms. Zbl 1277.03003
Espírito Santo, José; Ivetić, Jelena; Likavec, Silvia |
|
2012
|
Modal embeddings and calling paradigms. Zbl 1528.03123
Espírito Santo, José; Pinto, Luís; Uustalu, Tarmo |
|
2019
|
The \(\lambda \)-calculus and the unity of structural proof theory. Zbl 1187.68126
Espírito Santo, José |
|
2009
|
The polarized \(\lambda\)-calculus. Zbl 1394.68059
Espírito Santo, José |
|
2017
|
An isomorphism between a fragment of sequent calculus and an extension of natural deduction. Zbl 1023.03053
Santo, José Espírito |
|
2002
|
Structural proof theory as rewriting. Zbl 1151.03347
Espírito Santo, J.; Frade, M. J.; Pinto, L. |
|
2006
|
A calculus of multiary sequent terms. Zbl 1352.03063
Espírito Santo, José; Pinto, Luís |
|
2011
|
A refined interpretation of intuitionistic logic by means of atomic polymorphism. Zbl 1479.03006
Espírito Santo, José; Ferreira, Gilda |
|
2020
|
Plotkin’s call-by-value \(\lambda\)-calculus as a modal calculus. Zbl 1541.68084
Espírito Santo, José; Pinto, Luís; Uustalu, Tarmo |
|
2022
|
A coinductive approach to proof search. Zbl 1469.03041
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2013
|
Continuation-passing style and strong normalisation for intuitionistic sequent calculi. Zbl 1167.03012
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2007
|
Continuation-passing style and strong normalisation for intuitionistic sequent calculi. Zbl 1168.03008
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2009
|
Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search. Zbl 1456.03024
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2019
|
Towards a canonical classical natural deduction system. Zbl 1296.03011
Espírito Santo, José |
|
2013
|
Decidability of several concepts of finiteness for simple types. Zbl 1446.03036
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2019
|
Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications. Zbl 07649237
Espírito Santo, José; Frade, Maria João; Pinto, Luís |
|
2023
|
A faithful and quantitative notion of distant reduction for generalized applications. Zbl 07793034
Espírito Santo, José; Kesner, Delia; Peyrot, Loïc |
|
2022
|
Confluence and strong normalisation of the generalised multiary \(\lambda\)-calculus. Zbl 1100.03513
Espírito Santo, José; Pinto, Luís |
|
2004
|
The Russell-Prawitz embedding and the atomization of universal instantiation. Zbl 1494.03031
Santo, José Espírito; Ferreira, Gilda |
|
2021
|
Refocusing generalised normalisation. Zbl 1150.03336
Espírito Santo, José |
|
2007
|
Towards a canonical classical natural deduction system. Zbl 1287.03037
Espírito Santo, José |
|
2010
|
Monadic translation of intuitionistic sequent calculus. Zbl 1246.03027
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2009
|
Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications. Zbl 07649237
Espírito Santo, José; Frade, Maria João; Pinto, Luís |
|
2023
|
Plotkin’s call-by-value \(\lambda\)-calculus as a modal calculus. Zbl 1541.68084
Espírito Santo, José; Pinto, Luís; Uustalu, Tarmo |
|
2022
|
A faithful and quantitative notion of distant reduction for generalized applications. Zbl 07793034
Espírito Santo, José; Kesner, Delia; Peyrot, Loïc |
|
2022
|
The Russell-Prawitz embedding and the atomization of universal instantiation. Zbl 1494.03031
Santo, José Espírito; Ferreira, Gilda |
|
2021
|
A refined interpretation of intuitionistic logic by means of atomic polymorphism. Zbl 1479.03006
Espírito Santo, José; Ferreira, Gilda |
|
2020
|
Modal embeddings and calling paradigms. Zbl 1528.03123
Espírito Santo, José; Pinto, Luís; Uustalu, Tarmo |
|
2019
|
Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search. Zbl 1456.03024
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2019
|
Decidability of several concepts of finiteness for simple types. Zbl 1446.03036
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2019
|
The polarized \(\lambda\)-calculus. Zbl 1394.68059
Espírito Santo, José |
|
2017
|
A coinductive approach to proof search. Zbl 1469.03041
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2013
|
Towards a canonical classical natural deduction system. Zbl 1296.03011
Espírito Santo, José |
|
2013
|
Characterising strongly normalising intuitionistic terms. Zbl 1277.03003
Espírito Santo, José; Ivetić, Jelena; Likavec, Silvia |
|
2012
|
A calculus of multiary sequent terms. Zbl 1352.03063
Espírito Santo, José; Pinto, Luís |
|
2011
|
Towards a canonical classical natural deduction system. Zbl 1287.03037
Espírito Santo, José |
|
2010
|
The \(\lambda \)-calculus and the unity of structural proof theory. Zbl 1187.68126
Espírito Santo, José |
|
2009
|
Continuation-passing style and strong normalisation for intuitionistic sequent calculi. Zbl 1168.03008
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2009
|
Monadic translation of intuitionistic sequent calculus. Zbl 1246.03027
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2009
|
Delayed substitutions. Zbl 1203.68031
Espírito Santo, José |
|
2007
|
Completing Herbelin’s programme. Zbl 1215.03023
Espírito Santo, José |
|
2007
|
Continuation-passing style and strong normalisation for intuitionistic sequent calculi. Zbl 1167.03012
Espírito Santo, José; Matthes, Ralph; Pinto, Luís |
|
2007
|
Refocusing generalised normalisation. Zbl 1150.03336
Espírito Santo, José |
|
2007
|
Structural proof theory as rewriting. Zbl 1151.03347
Espírito Santo, J.; Frade, M. J.; Pinto, L. |
|
2006
|
Confluence and strong normalisation of the generalised multiary \(\lambda\)-calculus. Zbl 1100.03513
Espírito Santo, José; Pinto, Luís |
|
2004
|
Permutative conversions in intuitionistic multiary sequent calculi with cuts. Zbl 1041.03040
Espírito Santo, José; Pinto, Luís |
|
2003
|
An isomorphism between a fragment of sequent calculus and an extension of natural deduction. Zbl 1023.03053
Santo, José Espírito |
|
2002
|
Revisiting the correspondence between cut elimination and normalisation. Zbl 0973.03073
Espírito Santo, José |
|
2000
|