1,435 research outputs found
The Isabelle formalization of an incremental coniductive proof system
No full textSubmitted by Andrei Popescu ([email protected]) on 2010-01-28T22:08:37Z
No. of bitstreams: 1
CoinductiveProofSystem_in_Isabelle.zip: 771578 bytes, checksum: b4db9ac4c7487d058d4e57953e928045 (MD5)Made available in DSpace on 2010-01-28T22:08:37Z (GMT). No. of bitstreams: 1
CoinductiveProofSystem_in_Isabelle.zip: 771578 bytes, checksum: b4db9ac4c7487d058d4e57953e928045 (MD5)
Previous issue date: 2010-01-28unpublishe
The Isabelle formalization of a general theory of syntax with bindings, with lambda-calculus case studies included
No full textThis document presents and Isabelle formalization of a general theory of syntax with bindings. It also includes some case studies from the theory of lambda-calculus.not peer reviewedSubmitted by Andrei Popescu ([email protected]) on 2010-12-01T16:03:30Z
No. of bitstreams: 1
Lambda.zip: 1892882 bytes, checksum: b7a0d171aa35c9673addac6ef5f483c5 (MD5)Made available in DSpace on 2010-12-01T16:03:30Z (GMT). No. of bitstreams: 1
Lambda.zip: 1892882 bytes, checksum: b7a0d171aa35c9673addac6ef5f483c5 (MD5)
Previous issue date: 2010unpublishe
The Isabelle formalization of a general theory of syntax with bindings
No full textThis is a browsable html document presenting an Isabelle formalization of a general theory of syntax with static bindings and substitution.not peer reviewedSubmitted by Andrei Popescu ([email protected]) on 2010-12-01T15:56:31Z
No. of bitstreams: 1
Binding_Syntax.zip: 2522934 bytes, checksum: 0bc00207779bea85cf9ac644ec66dbff (MD5)Made available in DSpace on 2010-12-01T15:56:31Z (GMT). No. of bitstreams: 1
Binding_Syntax.zip: 2522934 bytes, checksum: 0bc00207779bea85cf9ac644ec66dbff (MD5)
Previous issue date: 2010unpublishe
HOAS on top of FOAS formalized in Isabelle/HOL
No full text"This collection of documents presents the Isabelle formalization of Higher-Order Abstract Syntax (HOAS) as a definitional layer on top of First-Order Abstract Syntax (FOAS). The formal scripts shown here are provided as a technical companion to the paper ""HOAS on top of FOAS"" to be presented at LICS 2010 (and to its more detailed technical report version). They work with Isabelle2009-1. The scripts are currently under (intensive!) development. To obtain the latest version of the theory, please contact the author at [email protected]."Submitted by Andrei Popescu ([email protected]) on 2010-04-30T20:52:24Z
No. of bitstreams: 1
HOASOnTopOfFOAS.zip: 3276637 bytes, checksum: 4fb0f88daf1c22f0203faa10ef17ed44 (MD5)Made available in DSpace on 2010-04-30T20:52:24Z (GMT). No. of bitstreams: 1
HOASOnTopOfFOAS.zip: 3276637 bytes, checksum: 4fb0f88daf1c22f0203faa10ef17ed44 (MD5)
Previous issue date: 2010unpublishe
- …
