Document Search Results

Al Wardani, Farah; Chaudhuri, Kaustuv; Miller, Dale

Formal reasoning using distributed assertions. (English) Zbl 1540.68253

Sattler, Uli (ed.) et al., Frontiers of combining systems. 14th international symposium, Frocos 2023, Prague, Czech Republic, September 20–22, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14279, 176-194 (2023).

MSC: 68V15 03B35

Cite Review PDF

Full Text: DOI

OA License

Urciuoli, Sebastián

A formal proof of the strong normalization theorem for system T in Agda. (English) Zbl 07810647

Nantes-Sobrinho, Daniele (ed.) et al., Proceedings of the 17th international workshop on logical and semantic frameworks with applications, LSFA, Belo Horizonte, Brazil, September 23–24, 2022. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 376, 81-99 (2023).

MSC: 68V15

Cite Review PDF

Full Text: DOI arXiv

Popescu, Andrei

Rensets and renaming-based recursion for syntax with bindings extended version. (English) Zbl 07722430

J. Autom. Reasoning 67, No. 3, Paper No. 23, 27 p. (2023).

MSC: 68V15

Cite Review PDF

Full Text: DOI

OA License

Popescu, Andrei

Rensets and renaming-based recursion for syntax with bindings. (English) Zbl 07628212

Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 618-639 (2022).

MSC: 68V15

Cite Review PDF

Full Text: DOI arXiv

OA License

Copello, Ernesto; Szasz, Nora; Tasistro, Álvaro

Formalization of metatheory of the lambda calculus in constructive type theory using the barendregt variable convention. (English) Zbl 1529.03126

Math. Struct. Comput. Sci. 31, No. 3, 341-360 (2021).

MSC: 03B40 68V15 68V20

Cite Review PDF

Full Text: DOI

Allais, Guillaume; Atkey, Robert; Chapman, James; McBride, Conor; McKinna, James

A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. (English) Zbl 1522.68118

J. Funct. Program. 31, Paper No. e22, 55 p. (2021).

MSC: 68N18 68N15 68N30 68Q55

Cite Review PDF

Full Text: DOI arXiv

Errington, Jacob; Jang, Junyoung; Pientka, Brigitte

Harpoon: mechanizing metatheory interactively. (English) Zbl 1540.68266

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 636-648 (2021).

MSC: 68V15

Cite Review PDF

Full Text: DOI

OA License

Urciuoli, Sebastián; Tasistro, Álvaro; Szasz, Nora

Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda. (English) Zbl 1498.03044

Nalon, Cláudia (ed.) et al., Proceedings of the 15th international workshop on logical and semantic frameworks, with applications, LSFA 2020, virtual workshop, August 27–28, 2020. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 351, 187-203 (2020).

MSC: 03B40 03F05

Cite Review PDF

Full Text: DOI

Found 8 Documents (Results 1–8)

Formal reasoning using distributed assertions. (English) Zbl 1540.68253

A formal proof of the strong normalization theorem for system T in Agda. (English) Zbl 07810647

Rensets and renaming-based recursion for syntax with bindings extended version. (English) Zbl 07722430

Rensets and renaming-based recursion for syntax with bindings. (English) Zbl 07628212

Formalization of metatheory of the lambda calculus in constructive type theory using the barendregt variable convention. (English) Zbl 1529.03126

A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. (English) Zbl 1522.68118

Harpoon: mechanizing metatheory interactively. (English) Zbl 1540.68266

Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda. (English) Zbl 1498.03044

Filter Results by …

Document Type

Author

Serial

Year of Publication

Main Field

Software