Document Search Results

Gabbay, Murdoch J.; Mulligan, Dominic P.

Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms. (English) Zbl 1186.68102

Inf. Comput. 208, No. 3, 230-258 (2010); corrigendum ibid. 212, 119 (2012).

MSC: 68N18

Cite Review PDF

Full Text: DOI

Nanevski, Aleksandar; Pfenning, Frank; Pientka, Brigitte

Contextual modal type theory. (English) Zbl 1367.03060

ACM Trans. Comput. Log. 9, No. 3, Article No. 23, 49 p. (2008).

MSC: 03B70 03B45 68N17 68N18

Cite Review PDF

Full Text: DOI Link

Morris, Peter; Altenkirch, Thorsten; McBride, Conor

Exploring the regular tree types. (English) Zbl 1172.68401

Filliâtre, Jean-Christophe (ed.) et al., Types for proofs and programs. International workshop, TYPES 2004, Jouy-en-Josas, France, December 15–18, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-31428-8/pbk). Lecture Notes in Computer Science 3839, 252-267 (2006).

MSC: 68N18 68N30

Cite Review PDF

Full Text: DOI

Ayala-Rincón, Mauricio; de Moura, Flávio L. C.; Kamareddine, Fairouz

Comparing and implementing calculi of explicit substitutions with eta-reduction. (English) Zbl 1067.03042

Ann. Pure Appl. Logic 134, No. 1, 5-41 (2005).

MSC: 03B70 03B40 68N18 68Q42

Cite Review PDF

Full Text: DOI

Ayala-Rincón, Mauricio; De Moura, Flávio L. C.; Kamareddine, Fairouz

Comparing calculi of explicit substitutions with eta-reduction. (English) Zbl 1261.03071

de Queiroz, Ruy (ed.) et al., WoLLIC’2002. Proceedings of the 9th workshop on logic, language, information and computation, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio), Rio de Janeiro, Brazil, July 30–August 2, 2002. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 67, 76-95 (2002).

MSC: 03B40 68N18

Cite Review PDF

Full Text: DOI

Coquand, Catarina

A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions. (English) Zbl 1041.68016

High.-Order Symb. Comput. 15, No. 1, 57-90 (2002).

MSC: 68N18

Cite Review PDF

Full Text: DOI

Duggan, Dominic

Higher-order substitutions. (English) Zbl 1003.68024

Inf. Comput. 164, No. 1, 1-53 (2001).

MSC: 68N18 03B40

Cite Review PDF

Full Text: DOI Link

Muñoz, C.

Proof-term synthesis on dependent-type systems via explicit substitutions. (English) Zbl 0989.68019

Theor. Comput. Sci. 266, No. 1-2, 407-440 (2001).

MSC: 68N18

Cite Review PDF

Full Text: DOI

Schürmann, C.; Despeyroux, J.; Pfenning, F.

Primitive recursion for higher-order abstract syntax. (English) Zbl 0994.68028

Theor. Comput. Sci. 266, No. 1-2, 1-57 (2001).

MSC: 68N18

Cite Review PDF

Full Text: DOI

Muñoz, César

Dependent types and explicit substitutions: A meta-theoretical development. (English) Zbl 0976.03014

Math. Struct. Comput. Sci. 11, No. 1, 91-129 (2001).

Reviewer: Paula G.Severi (Montevideo)

MSC: 03B40 68N18

Cite Review PDF

Full Text: DOI

Despeyroux, Joëlle; Leleu, Pierre

A modal lambda calculus with iteration and case constructs. (English) Zbl 0943.03010

Altenkirch, Thorsten (ed.) et al., Types for proofs and programs. International workshop, TYPES ’98. Kloster Irsee, Germany, March 27-31, 1999. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1657, 47-61 (1999).

MSC: 03B40 68N18

Cite Review PDF

Strecker, Martin; Luther, Marko; von Henke, Friedrich

Interactive and automated proof construction in type theory. (English) Zbl 0970.68150

Bibel, Wolfgang (ed.) et al., Automated deduction. A basis for applications. Vol. 2: Systems and implementation techniques. Dordrecht: Kluwer Academic Publishers; 0-7923-5132-0 (set)). Appl. Log. Ser. 9, 73-96 (1998).

MSC: 68T15 68N18

Cite Review PDF

Despeyroux, Joëlle; Pfenning, Frank; Schürmann, Carsten

Primitive recursion for higher-order abstract syntax. (English) Zbl 1063.03511

de Groote, Philippe (ed.) et al., Typed lambda calculi and applications. Third international conference on typed lambda calculi and applications, TLCA ’97, Nancy, France, April 2–4, 1997. Proceedings. Berlin: Springer (ISBN 3-540-62688-3/pbk). Lecture Notes in Computer Science 1210, 147-163 (1997).

MSC: 03B40 68N18 68N30

Cite Review PDF

Coquand, Catarina

From semantics to rules: a machine assisted analysis. (English) Zbl 0953.68569

Börger, Egon (ed.) et al., Computer science logic. 7th Workshop, CSL ’93, Swansea, GB, September 13-17, 1993. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 832, 91-105 (1994).

MSC: 68Q55 68N18

Cite Review PDF

Found 14 Documents (Results 1–14)

Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms. (English) Zbl 1186.68102

Contextual modal type theory. (English) Zbl 1367.03060

Exploring the regular tree types. (English) Zbl 1172.68401

Comparing and implementing calculi of explicit substitutions with eta-reduction. (English) Zbl 1067.03042

Comparing calculi of explicit substitutions with eta-reduction. (English) Zbl 1261.03071

A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions. (English) Zbl 1041.68016

Higher-order substitutions. (English) Zbl 1003.68024

Proof-term synthesis on dependent-type systems via explicit substitutions. (English) Zbl 0989.68019

Primitive recursion for higher-order abstract syntax. (English) Zbl 0994.68028

Dependent types and explicit substitutions: A meta-theoretical development. (English) Zbl 0976.03014

A modal lambda calculus with iteration and case constructs. (English) Zbl 0943.03010

Interactive and automated proof construction in type theory. (English) Zbl 0970.68150

Primitive recursion for higher-order abstract syntax. (English) Zbl 1063.03511

From semantics to rules: a machine assisted analysis. (English) Zbl 0953.68569

Filter Results by …

Document Type

Author

Serial

Year of Publication

Main Field

Software